Bartosz Milewski：初识类型论

我想让程序员初步了解类型论及其与数学基础的联系。目的地是恒等类型：在理论内部表达相等的一种方式。为此，我先介绍递归、依赖类型、归纳法和命题即类型。

考虑非正式等式 1 × A = A。在编程中，单位类型只有一个值，把它与 A 的一个元素配对不会增加信息。我们可以编写一个函数去掉单位值，再写一个函数把它加回来。

严格说来，这些函数提示的是同构，而不是自动相等：我们仍需要证明它们互为逆函数。在普通编程语言中，A 和由单位值与 A 构成的对并不一定能不经转换就相互替换。

我用两个构造器引入自然数：零和后继。零可以直接构造；后继接受一个自然数并构造另一个。重复应用就得到零、一、二等数。

类型还需要消去规则：如何定义一个接受自然数的函数？为零给出基础值，再给出从前一个结果得到下一个结果的步骤。两者共同定义递归函数。

计算规则规定所得函数在零和后继处如何工作。阶乘是一个例子：从 1 开始，每一步把前一个结果乘以下一个数。步骤本身不必写成递归函数。

按长度索引的向量展示了依赖类型。这里不是一个不区分长度的向量类型，而是一族由自然数长度索引的类型。空向量长度为零；向长度为 n 的向量添加元素，得到长度为 n+1 的向量。

结果类型依赖于值 n。这让类型检查器能够跟踪长度关系，从而根据类型规则拒绝长度不兼容的操作。这不同于只依赖另一个类型的类型，例如整数列表。

现在定义一个依赖于自然数的函数：对每个 n，它返回一个类型依赖于 n 的值。基础情况构造空向量；步骤接收长度为 n 的向量并添加指定元素，得到长度为 n+1 的向量。重复步骤就得到填满该元素的向量。

这种依赖消去器称为归纳。与普通递归相比，结果类型可以随输入变化。计算规则仍然规定零和后继情况下的行为。

命题即类型，也称 Curry–Howard 对应，把这一构造与证明联系起来。命题由类型表示，类型中的一个值可作为证明。例如，A 且 B 的证明对应一个包含 A 的证明和 B 的证明的对。

类型族 C(n) 可以表示每个自然数对应的命题。基础情况是 C(0) 的证明，步骤把 C(n) 的证明变成 C(n+1) 的证明。因此依赖消去器对应数学归纳法。

恒等类型表达类型 A 中两个值 x 和 y 相等的命题。由于命题随两个值变化，它是一个依赖类型族。恒等类型中的值是理论内部相等的证据。

基本构造器是自反性：对任意 x，refl(x) 是 x 等于自身的证据。我把由 x 和 y 索引的相等类型族想象成一个平面；自反性情形位于对角线上。这个图像帮助建立直觉，不能替代形式规则。

有趣的问题是消去：给定 x 等于 y 的证明 p，我们可以构造什么？这里的依赖类型族依赖 x、y 和相等证明 p。它比只依赖一个自然数的例子更一般。

对于自然数，消去器需要基础情况和后继情况。对于恒等类型，引入规则包含自反性情形。恒等消去器通常称为路径归纳，它允许我们通过指定自反性情形下的行为来定义依赖构造，同时遵守计算规则。

所得函数在给定 x、y 以及它们相等的证据 p 时适用。计算规则说明，当证据是 refl(x) 时，结果与为自反性提供的情况一致。这是一条形式规则，不应简化成“所有相等证明都相同”的说法。

演讲中，一位观众指出展示公式中的量词和作用域问题，我承认了这一更正。整体目标仍是把恒等消去器与前面介绍的归纳原理联系起来。

最后我借用同伦类型论的直觉：相等证明可以被建模为路径。把路径比作旅程、把自反性比作零长度路径，会让人联想到芝诺悖论；这只是说明思想的类比，不是对消去规则的推导。