在IDRIS中表达variadic函数的类型
在“使用IDRIS ”的“ 类型驱动的开发”一书中，作者解释了如何创建variadic函数。他以加法器函数为例，该函数消耗了第一个参数n：nat，然后 n + 1 整数参数要添加。为了声明此功能，该书介绍了相关类型adderType，以便可以写入：
adder: (numargs: Nat) -> (acc: Int) -> AdderType numargs
到目前为止还不错。但是，提出了以下adderType的定义：
AdderType : (numargs: Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next: Int) -> AdderType k
此时我迷路了。行adderType z = int是有道理的，但最后一个不。我以为表达式（下一个：int） - ＆gt; adderType k具有善良的int-＆gt;类型，但是不是 kint type。 idris是否认为任何因类型也是 的类型？如果是，这也适用于类型的构造函数？ （也就是说：类型类型 - ＆gt; type的值也有type？）
免责声明：我是初学者在类型理论中，我对“类型”和“依赖类型”等技术术语的使用可能是不合适的。如果是这种情况，请纠正我。
In the book "Type-Driven developement with Idris" the author explains how to create variadic functions. He takes the example of a adder function that consumes a first parameter n: Nat and then n + 1 integer parameters to be added. In order to declare this function the book introduces the dependent type AdderType so that one can write:
adder: (numargs: Nat) -> (acc: Int) -> AdderType numargs
So far so good. But then the following definition of AdderType is proposed:
AdderType : (numargs: Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next: Int) -> AdderType k
At this point I'm lost. Line AdderType Z = Int makes sense but the last one does not. I would have thought that the expression (next: Int) -> AdderType k had kind Int -> Type, but not kind Type. Does Idris consider that any dependent type is also a type? If yes, does that also apply to type constructor? (That is to say: does a value of kind Type -> Type also have kind Type ?)
Disclaimer: I'm a beginner in type theory so my usage of technical terms like "kind" and "dependent type" might be inappropriate. Please correct me if this is the case.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
最终，我理解了自己的错误，所以我要回答自己的问题，以防其他人感兴趣。我让
的类型（下一：int） - ＆gt; AdderType k（确实是 a 类型），的 value （next：int：int） - ＆gt; adderType k（ 类型int到类型adderType k的所有功能的类型）。正确的是，除addertype z外，所有定义的类型都是函数类型。但是无论如何，功能类型只是一种普通类型。我可以理解它的方式是想象如果我们可以单独定义每个
addertype k，那将是什么结果。这将是以下定义的无限列表：然后很明显，每个
addertype k确实只是一种普通类型。此外，每种新定义的类型都可以在以下行的右侧内使用：在这一点上，无限的定义列表（第一个）可以用单个多态定义代替。
Eventually I understood my mistake so I'm answering my own question just in case someone else might be interested. I was confusing the kind of
(next: Int) -> AdderType k(which is indeed a type) with the value of(next: Int) -> AdderType k(which is the type of all functions from typeIntto typeAdderType k). What is true is that all the defined types exceptAdderType Zare function types. But a function type is just a normal type anyway.The way I could make sense of it was by imagining what would be the result if we could define each
AdderType kindividually. It would be the infinite list of following definitions:It then became very obvious that each
AdderType kis indeed just a normal type. Furthermore each newly defined type could be used inside the right hand side of the following line:And at this point the infinite list of definitions (except the first) could be replaced by a single polymorphic definition.