多态类型论

多态类型论是一种简单类型 $\lambda$ 演算的扩展, 使其支持类型上的变量以及对这些变量进行替换操作的能力.

类型变量往往通过全称类型 (即类型上的全称量词) 引入, 此时全称量词给类型论带来的表达力增强叫做参数多态.

换言之, 我们应该能在多态类型论中讨论类似如下函数的事物:

$$f:\forall \alpha .\alpha \to \alpha$$

注 0.1. 注意这里并不意味着 $\forall \alpha .\alpha \to \alpha$ 这个表达式必须是类型, 它可以是一种独立于类型的概念, 使得 “函数定义” 可以进行这样的全称量化, 但全称量词并不在类型定义的一部分.

可以理解为该全称量词仅仅是二阶的, 而不是高阶的. 这种情况下类型上的全称量词叫类型范式.

在多态类型论中, 除了一般的变量之外, 还存在类型变量, 因此类型上的语法也复杂了起来, 因此它涉及的相继式中, 语境要包含类型变量和一般的变量:$$\Sigma ;\Gamma ⊢u:\alpha$$以上相继式中, $\Sigma$ 是类型变量的列表, $\Gamma$ 是一般变量的列表且可以使用 $\Sigma$ 中的类型变量, $\alpha$ 是在 $\Sigma$ 下合法的类型. 另外还需要描述类型本身的相继式, 语境只包含类型即可, 类似$$\Sigma ⊢\alpha$$

多态类型论是一种广泛的概念, 因此难以给出准确定义, 但它有诸多具体例子.

1例子

•	$\Pi$ 类型在参数类型是宇宙的情况下就是一种全称量词: $$\prod _{\alpha :\mathcal{U}}\alpha \to \alpha$$因此依值类型论往往都是多态类型论.

•	F 系统是经典的多态类型论.

•	Hindley–Milner 类型系统是一种弱于 F 系统的多态类型论, 拥有完整的类型推导.

2相关概念

•	除参数多态外还有其它的多态, 例如特设多态. 但 “多态” 一词往往特指参数多态.

•	参数性是支持全称量词的多态类型论重要的元性质, 相关证明手法叫 Tait 可计算性.

•	存在类型是可以用全称类型$\lambda$ 编码的一种类型.

术语翻译

多态类型论 • 英文 polymorphic type theory

参数多态 • 英文 parametric polymorphism

类型范式 • 英文 type scheme