Idris中的"half"函数类型签名

Question

我是Idris的新手,我正在尝试捕捉基本的概念和语法.

即使它听起来毫无意义,我也试图定义一个half将自然减半的函数.

我希望得到类似的东西:

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

但当然它不起作用.特别是我得到:

错误:预期:依赖类型签名

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

可能吗？

谢谢.

Answer 1

你想要的是表达那些持有的half n一些Nat乌拉尔数字.这样做的方法是使用sigma类型,即数字和证明的从属对(它是依赖对,因为第二个坐标的类型取决于第一个坐标的值).kn = k + kkn = k + kn = k + kk

Idris标准库定义DPair了从属对,包括允许您编写的一些语法糖

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

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

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

？