types - Idris 中的非零整数类型？

Question

我有一个函数，它返回一个应该是非零的整数，并希望通过它的返回类型来保证这一点。你如何表达 Idris 中非零整数的类型？

Answer 1

根据您的功能，有不同的方法。如果您使用 Nat作为返回类型，您可以阅读 Theorem Proving in the Idris Tutorial .一个例子是 inc这增加了 Nat和证明 incNotZ ，对于每个 n : Nat , Not (inc n = Z) :

inc : Nat -> Nat
inc n = S n

incNotZ : (n : Nat) -> Not (Z = inc n)
incNotZ n p = replace {P = incNotZTy} p ()
  where
    incNotZTy : Nat -> Type
    incNotZTy Z = ()
    incNotZTy (S k) = Void

有时您可以在结果旁边生成一个证明，例如:

data NotZero : Nat -> Type where
  MkNotZero : (n : Nat) -> NotZero (S n)

inc : (n : Nat) -> NotZero (S n)
inc n = MkNotZero n

rev : NotZero n -> Not (n = 0)
rev (MkNotZero n) = SIsNotZ -- from Prelude.Nat

这里 NotZero n是证明 n不为零，如 n只能通过 (S n) build .确实可以转换任何 NotZero n至 Not (n = 0)与 rev .

如果您的证明类型适合该功能，这通常是更好的选择。因为两者 inc和 NotZero有 (n : Nat) -> … (S n)您可以免费获得证明。另一方面，如果你想证明一个函数的某些东西，它拥有什么性质，比如 plus 的交换性或对称性，需要第一种方法。

如果您使用的是 Int作为返回类型，这通常没有用，因为 Int可以溢出， idris 不能争论 Int (或 Integer 或 Float 或……):

*main> 10000000000000000000 * (the Int 5)
-5340232221128654848 : Int

所以通常的方法是在运行时构造一个证明来查看非零性是否成立:

inc' : Int -> Int
inc' i = abs i + 1

incNotZ' : (i : Int) -> Either (So (inc' i == 0)) (So (not (inc' i == 0)))
incNotZ' i = choose (inc' i == 0)

然后，当您调用 incNotZ' 时，您可以匹配结果以获得右侧的证明或处理左侧的错误情况。

例如，如果您使用的是非溢出 Integer并且真的非常确定您的函数永远不会返回 0，您可以强制编译器相信您:

inc' : Integer -> Integer
inc' i = abs i + 1

incNotZ' : (i : Integer) -> Not (0 = inc' i)
incNotZ' i = believe_me