Idris的'half'功能类型签名

我是Idris的新手，我试图去捕捉基本概念和语法。Idris的'half'功能类型签名

即使它听起来毫无意义，我试图定义一个将自然减半的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) 

这可能吗？

谢谢。

来源

2016-11-30 Cristiano Paris

你想要什么来表达half n一些Nat乌拉尔号k这样n = k + k成立。的方式做到这一点是通过使用sigma type，即依赖对一号码k和证明n = k + k（这是一个依赖对因为类型的秒坐标的，n = k + k依赖于值的第一坐标， k）。

的伊德里斯标准库depedent对定义DPair，包括一些语法糖，让您写

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

但是，请注意，您将无法实现half（作为一个整体功能），因为有没有好的答案例如half 1。也许你想要的是

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

？

来源

2016-12-01 02:00:46 Cactus

嗯，谢谢，它确实是typechecks。无论如何，我想要表达的是类似“half：（n：Nat） - > Even n - > Nat”的信息，因为生成的“Nat”实际上是第一个“Nat”的一半。在你的情况下，函数总数是多少（即只接受输入甚至是'Nat'）？你使用Eirther这个事实让我觉得它不是，而在第一个版本中，我们必须提供一半带有证明的'n'，即偶数，这就省去了1，3和所有其他的奇数。再次感谢你的帮助。 –

第二个版本可以做成总数，因为每个'n'都是'2 * k'或'2 * k + 1'。当然，第一个不能，因为没有'k'，例如， '1 = 2 * k'。 – Cactus

您不应该使用k两次。（n：Nat） - >（k：Nat） - >（n = k + k） - > Nat 是正确的，但是没用。我认为你需要一半：（n：Nat） - >也许（k ** n = k + k）

来源

2017-11-02 10:11:58

Idris的'half'功能类型签名

回答

相关问题