在 Idris 中表达可变参数函数的类型

Question

在“使用 Idris 进行类型驱动开发”一书中，作者解释了如何创建可变参数函数。他以adder 函数为例，该函数使用第一个参数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 行有意义，但最后一行没有。我会认为表达式(next: Int) -> AdderType k 有亲切的Int -> Type，但不是 亲切的Type。 Idris 是否认为任何依赖类型也是也是一种类型？如果是，这是否也适用于类型构造函数？ （也就是说：kind Type -> Type 的值是否也有 kind Type ？）

免责声明：我是类型论的初学者，所以我对“种类”和“依赖类型”等技术术语的使用可能不合适。如果是这种情况，请纠正我。

Answer 1

最终我理解了我的错误，所以我正在回答我自己的问题，以防其他人可能感兴趣。我将(next: Int) -> AdderType k 的种类（确实是a 类型）与(next: Int) -> AdderType k 的值（即从Int 类型到AdderType k 类型的所有函数的 类型）。真实的是，除AdderType Z 之外的所有已定义类型都是函数类型。但无论如何，函数类型只是普通类型。

我理解它的方式是想象如果我们可以单独定义每个 AdderType k 会产生什么结果。这将是以下定义的无限列表：

AdderType Z = Int
AdderType (S Z) = Int -> Int
AdderType (S (S Z)) = Int -> Int -> Int
AdderType (S (S (S Z))) = Int -> Int -> Int -> Int
…

然后很明显每个AdderType k 确实只是一个普通类型。此外，每个新定义的类型都可以在以下行的右侧使用：

AdderType Z = Int
AdderType (S Z) = Int -> AdderType Z
AdderType (S (S Z)) = Int -> AdderType (S Z)
AdderType (S (S (S Z))) = Int -> AdderType (S (S Z))
…

此时，无限的定义列表（第一个除外）可以被多态定义替换。

AdderType Z = Int
AdderType (S k) = Int -> AdderType k