如何解决伊德里斯将非线性论证解释为线性
我正在使用 Idris2 从 TDD 和 idris book 中工作,在第 6 章我们编写了一个函数,该函数将动态数量的数字相加。这是我的实现,只有 Int
s:
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 举报,一经查实,本站将立刻删除。