Idris可变参数函数AdderType定义的Kind判定规则疑问

你理解卡壳的根源是对(next: Int) -> AdderType k的Kind判断出错了，先把Idris里Kind层级的最基础规则说清楚：

• 只要一个表达式能直接写在值的类型标注位置（也就是冒号右边），它的Kind就是Type。不管这个类型是普通基础类型、普通函数类型，还是依赖函数类型，都遵守这个规则。
• 你把「类型构造函数」和「依赖函数类型本身」搞混了，才会误判它的Kind：
  • 如果是lambda写法\(next: Int) => AdderType k，这是个接收Int值、返回类型的类型级函数，它的Kind确实是Int -> Type，这种东西不能直接给普通值当类型用。
  • 但定义里写的(next: Int) -> AdderType k是依赖函数类型本身，描述的是「接收一个名为next的Int参数，返回一个AdderType k类型的值」的函数值的类型，这类函数是可以直接定义、调用的普通运行时值，描述它的类型自然属于Type层级。

代入具体值展开就很容易理解 #

我们给AdderType传入不同的Nat参数手动展开，逻辑完全通顺：

• 传入Z（自然数0）：AdderType Z = Int，对应不需要再接额外参数，直接返回累加的Int结果，Kind是Type，和你理解的一致。
• 传入S Z（自然数1）：AdderType (S Z) = (next: Int) -> AdderType Z = Int -> Int，这是接收1个Int、返回Int的函数类型，Kind是Type。
• 传入S (S Z)（自然数2）：AdderType (S (S Z)) = (next: Int) -> AdderType (S Z) = Int -> Int -> Int，这是接收2个Int、返回Int的柯里化函数类型，Kind是Type。
• 以此类推，不管传入的n是多少，AdderType n展开后永远是「接收n个Int参数、最终返回Int」的柯里化函数类型，全都是Type层级的合法类型，完全匹配它的声明AdderType : (numargs: Nat) -> Type。

对你两个补充问题的明确答复 #

• 不存在“所有依赖类型都归为Type”的规则：只有能直接作为值的类型标注的依赖类型，Kind才是Type；如果是接收参数产出类型的类型级函数，它的Kind是对应参数到Type的函数类型，不属于Type。
• Kind为Type -> Type的值（比如List、Maybe这类泛型类型构造器）不属于Kind Type。你没法直接定义一个类型为List的值，必须传入具体类型参数得到List Int这类结果，才是能给值用的合法类型，这也刚好符合前面说的Kind判断规则。

  你可以直接在Idris REPL里验证：输入:t List会返回List : Type -> Type；输入:t Int返回Int : Type；输入:t (Int -> Int)返回Int -> Int : Type，和结论完全对应。

内容的提问来源于stack exchange，提问作者Contactomorph