Idris中非零整数的类型?

根据您的功能,有不同的方法。如果您使用 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) . 事实上,一个人可以改变任何 非零n 到 Not (n = 0) 具有 rev .

如果您的证明类型适合功能,这通常是更好的选择。因为两者 股份有限公司 和 NotZero 有 (n : Nat) -> … (S n) 你可以免费得到证据。另一方面,如果你想证明一个函数,它有什么性质,比如 plus ,需要第一种方法。

如果你正在使用 Int 作为返回类型,这通常不有用,因为 内景 can溢出,Idris无法争论 内景 (或 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时,你可以匹配结果,在右边得到证明,或者在左边处理错误案例。

例如,如果使用非溢出 整数 如果确实非常确定函数永远不会返回0,则可以强制编译器相信您:

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

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