伊德里斯将非线性论证解释为线性

问题描述

我正在使用 Idris2 从 TDD 和 idris book 中工作，在第 6 章我们编写了一个函数，该函数将动态数量的数字相加。这是我的实现，只有 Ints:

AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = Int -> AdderType k

adder : (numargs : Nat) -> Int -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

请注意，(S k) 的 adder 情况返回一个 lambda。我试图将 next 添加到 adder 的参数中：

adder : (numargs : Nat) -> Int -> AdderType numargs
adder Z acc = acc
adder (S k) acc next = adder k (next + acc)

但是当我尝试编译这个 idris2 时出现以下错误。

Error: 
While processing right hand side of adder. 
Trying to use linear name next in non-linear context.

 24 | adder : (numargs : Nat) -> Int -> AdderType numargs
 25 | adder 0 acc = acc
 26 | adder (S k) acc next = adder k (next + acc)
                                      ^^^^

为什么在这种情况下 idris2 决定 next 是线性的，而我没有明确说明它是？这是一个错误吗？

注意：如果我对书中列出的更通用的实现做同样的事情：

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

adder : Num numType => (numargs : Nat) -> numType -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc next = adder k (next + acc)

我收到以下错误：

Error: While processing left hand side of adder. Unsolved holes:

Tri.{argTy:4060} introduced at:
/home/stefan/dev/tdd-idris/Tri.idr:25:1--25:6
 21 | AdderType (S k) numType = (next : numType) -> AdderType k numType
 22 |
 23 | adder : Num numType => (numargs : Nat) -> numType -> AdderType numargs numType
 24 | adder Z acc = acc
 25 | adder (S k) acc next = adder k (next + acc)
      ^^^^^

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）