参数性

在多态类型论中, 参数性概括了 “对类型变量什么都不能做” 的思想. 例如, 假设我们有如下函数:

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

参数性认为, 既然 $f$ 对 $\alpha$ 什么都不能做, 因此它唯一能做的事情是原封不动返回它的参数. 这种思想和$\lambda$ 编码密切相关.

该性质需要语义工具证明 (Tait 可计算性), 且有多种应用.

1例子

抽象类型

我们可以抽象地看待自然数: 任何类型 $\alpha$ 配备上如下操作$$\begin{array}{rl}& z:\alpha \\ & s:\alpha \to \alpha \end{array}$$都是一种 “自然数”. 我们用如下符号表示:$$\mathbb{N}:=\left\{\begin{array}{l}\alpha :\mathcal{U}\\ z:\alpha \\ s:\alpha \to \alpha \end{array}\right\}$$当然也可以省略操作的名字, 并使用$\Sigma$ 类型、积类型等构造, 写作 $\mathbb{N}:={\sum }_{\alpha :\mathcal{U}}\alpha \times (\alpha \to \alpha )$.

在有了抽象的自然数后, 我们可以将它具体化. 假设我们有整数的类型, 记作 $\mathbb{Z}$, 且上面有已经定义好的加减乘除. 用这个整数就可以 “实现” 自然数所需的全部操作:

$$\begin{array}{rl}& {\mathbb{N}}_{\mathbb{Z}}:\mathbb{N}\\ & {\mathbb{N}}_{\mathbb{Z}}:=\left\{\begin{array}{l}\alpha =\mathbb{Z}\\ z=0\\ s=\lambda x.x+1\end{array}\right\}\end{array}$$

虽然 $\alpha =\mathbb{Z}$ 的实例可能出现负数, 但我们如果只使用 $\mathbb{N}$ 里的操作, 就一定不可能构造出负数来, 因为我们在使用 $\mathbb{N}$ 时不知道里面的 $\alpha$ 到底是什么, 无法做到 “看透它内部实际上是整数并构造出负数” 这样的事情.

免费定理

参数性的思想可以对一些类型直接给出定理.

•	考虑类型 $\forall a.a$, 它可以解读为 “对所有类型都给出其实例”, 然而它内部不可能知道这个类型是什么, 因此不可能有这样的操作, 因此该类型等价于空类型.

•	考虑类型 $\forall a.a\to a$, 它可以解读为 “对任意类型, 给出该类型到它自己的映射”, 然而它内部不可能知道这个类型是什么, 因此接受到 $a$ 的实例后只能原封不动地返回, 因此该类型只有唯一实例, 等价于单位类型.

2定义

(..)

构造

(..)

内化

(..)

术语翻译

参数性 • 英文 parametricity

抽象类型 • 英文 abstract type