idris - 伊德里斯将非线性参数解释为线性

Question

我正在使用 Idris2 编写带有 idris 的 TDD 书，在第 6 章中，我们编写了一个函数，可以将动态数量的数字彼此相加。这是我只有Ints 的 impl：

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)

请注意，返回 lambda的(S k)情况。adder我试图只添加next到加法器的参数：

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)
                                      ^^^^

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

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

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)
      ^^^^^

标签： idrislinear-types