dependent-type - Idris 中的“半”函数类型签名

Question

我对 Idris 很陌生，我正在尝试了解基本概念和语法。

即使这听起来毫无意义，我还是试图定义一个 half功能是自然减半。

我想想出类似的东西:

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)

但当然它不起作用。具体我得到:

error: expected: dependent type signature

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)

是否可以？

谢谢。

Answer 1

你要表达的是half n是一些 Nat乌拉尔号码k使得 n = k + k持有。方法是使用 sigma type ，即数字的依赖对 k和证明 n = k + k (它是一个依赖对，因为第二个坐标的类型 n = k + k 取决于第一个坐标的值 k )。

Idris 标准库定义了 DPair 对于依赖对，包括一些允许您编写的语法糖

half : (n : Nat) -> (k ** n = k + k)

但是，请注意，您将无法实现 half (作为一个总功能)因为没有很好的答案，例如 half 1 .也许你想要的是

half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1))

?