Kind 与类型算子

把List想成一个留有空格的类型模板。填入Int得到整数列表，填入Bool得到布尔列表。List本身还没说元素是什么，因而不能在这个系统里直接写一个普通变量声明 xs:List。

Pair留有两个空格。先填Int得到 Pair Int:*→*，还可以再填Bool得到 Pair Int Bool:*。部分应用没有失败，只是结果仍是类型算子。

类型层的λ与λ演算公理库λ 演算Lambda calculus · Untyped lambda calculus以变量、抽象、应用和 β-归约表达高阶函数计算的无类型核心演算。形式相似，不过参数是类型表达式而不是运行时整数或函数值。λX:*.Pair X Bool描述“把X与Bool配成一对”的类型变换；它没有分配一个二元组，也没有创建一个运行时闭包。

一个接收类型算子的算子 ​

考虑

逐步检查：在 $F:\ast \to \ast$ 的环境下，Int的kind为 $\ast$；应用规则给出 $F\mathrm{Int}:\ast$；移去F假设并作类型抽象，得到

于是K List合法，结果是List Int。K (Pair Bool)也合法，结果是Pair Bool Int。K Int则不合法，因为K要求的实参kind是 $\ast \to \ast$，Int只具有 $\ast$。

下面四个判断把“尚未填完”与“填错位置”分开：

List Int和List Bool的kind相同，类型却不同。Kind检查只保证类型表达式的接口匹配，不把同一kind内的所有类型判作相等；正如3和true都能出现于程序中，也不能据此认为它们类型相同。

三层对象不要互换 ​

3:Int是项判断，Int:*是类型表达式的kind判断。这里的 $\ast$ 不是Int的一个运行时值，也不是本页语言里可自行应用的类型算子。

本页只允许类型依赖类型，类型算子不能读取一个普通项变量n来计算“长度恰为n的数组类型”。那需要另行加入依赖项的类型规则。Kind与依赖类型中的宇宙也有联系，但简单箭头kind分类并不包含宇宙提升、累积性或 Type_i:Type_{i+1} 的规则，不能只凭“类型的类型”这句口号混用两套体系。

Kind检查可以按类型表达式的语法树递归执行：变量查Δ，应用先检查函数kind再比较参数kind，抽象扩展Δ。每一步下降到严格子表达式，因此对本页有限语法总会结束。检查器遇到 List List 时能在类型层报错，不必等待项级检查才发现问题。

System F公理库System FSystem F · Polymorphic lambda calculus具有显式类型抽象与类型应用的二阶多态 λ 演算。只对普通类型量化；若还允许项在 $F:\ast \to \ast$ 这样的算子上多态，就得到System Fω公理库System FωSystem F omega · Fω在显式System F中加入kind分类的类型算子、类型级β计算与高阶类型量化。的一项关键扩展。容器接口可以用F A统一表示不同容器形状，但知道F的kind并不自动获得映射、遍历或比较操作；这些仍需函数参数、字典或其他接口证据。

一个实用自检是：对每个类型参数同时写出名字和kind。若接口接收的是List，就写 $F:\ast \to \ast$；若接收的是List Int，就写 $A:\ast$。这个区分能在设计接口时暴露“传模板”与“传模板实例”的混淆。