System F

Leasier · 2026-08-20 16:57:12 · 算法·理论

System F / 多态 λ 演算

全称类型 (Universal Types)

观察习以为常的恒等函数 id_T = λx:T. x，尽管 T 不同时的实现别无二致，但在 STLC 中，我们却需要对每个 T 分别实现一个 id_T。\ 软件工程中有所谓 抽象原则 (abstraction principle)：即每一段重要的功能只在一处实现。依照这个思路，我们能不能将 T 抽象出去呢？

“将同一段代码在不同类型上复用”即所谓 多态 (polymorphism)，典型的有以下三类：

参数化多态 (parametric polymorphism)：使用全称量词泛化类型，对不同类型而言行为一致，典型的例子如上面的 id = λT. λx:T. x。\ Rmk. 直觉上讲，参数化多态的实现在某种程度上是“类型无关”的、或者说是“自然”的。后面会进一步加以讨论。\ 专用多态 (Ad-hoc polymorphism)：给不同类型对应的代码指定不同的行为，典型的例子如 OOP 中的 重载 (overloading)。\ 子类型多态 (subtype polymorphism)：通过子类关系允许在代码调用时泛化类型。

形式化

1. 语法形式

2. 类型规则

3. 计算规则

接下来利用上面的形式化规则小试牛刀：

• 试推导 \text{selfApp} = \lambda x : (\forall X. X \to X). \ x \ [\forall X. X \to X] \ x 的类型。

乍一看这不是我们在递归类型那一节提到的发散项 \omega 吗？事实上，不考虑递归类型的话，在 System F 中我们也是可以给 \text{selfApp} 赋予类型的：

• 利用 \text{T-TApp} 得到 x : (\forall X. X \to X) \vdash x \ [\forall X. X \to X] : (\forall X. X \to X) \to (\forall X. X \to X)。
• 再利用 \text{T-App} 得到 x : (\forall X. X \to X) \vdash x \ [\forall X. X \to X] \ x : \forall X. X \to X。
• 最后利用 \text{T-Abs} 得到 \varnothing \vdash (\lambda x : (\forall X. X \to X). \ x \ [\forall X. X \to X] \ x) : (\forall X. X \to X) \to (\forall X. X \to X)。

与此同时，我们前面定义了多态恒等函数 \text{id} : \forall X. X \to X，将其应用于 \text{selfApp} 上，根据定义立刻得到 \text{selfApp} \ \text{id} = \text{id}。直观上这的确是符合语义的，因为给 \text{id} 传入任何参数——包括它自己——都应该不变。

那 System F 的强约简性是不是已经被破坏了呢？事实上此处不足为证：因为 \text{selfApp} \ \text{selfApp} 并不能被赋予类型。

接下来留意到并非所有合于前述语法的类型都是良构的：比如 \forall X. \ Y \to X 中自由 类型变量 (type variable) Y 未被绑定——这也意味着前面的类型规则缺少了一些限制（只是 \text{selfApp} 的推导不涉及），下面也会补上。

4. 类型良构规则

Rmk. 若此处不改 \text{T-Var}，有反例：设 \Gamma = \{x : X\}，此时不应当有 \Gamma \vdash x : X，因为在这一上下文中 X 未被绑定。

Rmk. 下面还是默认使用 Barendregt 约定：同一上下文中绑定变量与自由变量的名称不会冲突。

引理：类型实例化保持良构性

若 \Gamma, X \vdash T \text{ type} 且 \Gamma \vdash S \text{ type}，则 \Gamma \vdash [X \mapsto S] T \text{ type}。

Proof. 对 T 的构造归纳即可。

定理：类型规则的正则性 (regularity)

若 \Gamma \vdash t : T，则 \Gamma \vdash T \text{ type}。

Proof. 对类型推导归纳即可，其中 \text{T-TApp} 的情形需要用到上面的引理。

例子：多态列表

将 List 视作类型算子，假设以下原语存在：

则我们可以写出多态版本的 map：

邱奇编码 (Church encodings) 举隅 (1)

首先回顾一下经典的丘奇布尔：

tru = λt. λf. t
fls = λt. λf. f
test = λb. λm. λn. b m n

考虑在 System F 中这样构造布尔类型：

再回顾一下布尔作为原语时的消除规则：

可以发现这跟 test 在 System F 中的类型刚好对上了！这也提示我们：

类型的消除无非是应用一个根据消除规则构造的多态函数。

Rmk. 在 严格求值 的语境下，test [T] t1 t2 t3 必须要在 t2 和 t3 都求值完成才开始求值，但这是与 if 的语义不符的。\ 若要坚持严格求值，一个可行的解决方案是使用 无效抽象 (dummy abstraction) 延后求值，就像我们先前在 FP 中模拟 OOP 那样：

\begin{aligned} \text{CBool} &= \forall X. \ (\text{Unit} \to X) \to (\text{Unit} \to X) \to X \\ \text{tru} &= \lambda X. \ \lambda t : (\text{Unit} \to X). \ \lambda f : (\text{Unit} \to X). \ t \ \text{unit} \\ &: \text{CBool} \\ \text{fls} &= \lambda X. \ \lambda t : (\text{Unit} \to X). \ \lambda f : (\text{Unit} \to X). \ f \ \text{unit} \\ &: \text{CBool} \\ \text{test} &= \lambda X. \ \lambda b : \text{CBool} . \ \lambda m : \text{Unit} \to X. \ \lambda n : \text{Unit} \to X. \ b \ [X] \ m \ n \\ &: \forall X. \ \text{CBool} \to (\text{Unit} \to X) \to (\text{Unit} \to X) \to X \end{aligned}

此时 if t1 t2 t3 即等价于 test [T] t1 (λ_:Unit. t2) (λ_:Unit. t3)。

接下来在布尔之外的其他非递归类型上牛刀小试。

先回顾一下 Unit 作为原语时的消除规则：

在 System F 中这样构造 Unit 类型：

可以发现 unit 就是多态恒等函数，且 seq 和 let unit = ... in ... 的效果是一样的——它什么都不改变。

再看积类型作为原语时的引入和消除规则：

在 System F 中这样构造积类型：

Rmk. 目前 \text{CPair} \ T_1 \ T_2 的写法并不正式，因为我们没有引入“类型的应用”；后面我们将会正式讨论这样的 类型算子 (type operator)。

最后看和类型作为原语时的引入和消除规则：

在 System F 中这样构造和类型：

Rmk. 若取 T_1 = T_2 = \text{Unit}，可以发现 T_1 + T_2 得到的正是前面添加无效抽象后的丘奇布尔。

最后来讨论一些基本的归纳类型。我们先回顾一下最基本的递归类型——自然数——的邱奇编码的构造：

zero = λs. λz. z
succ = λn. λs. λz. s (n s z)

观察自然数的消除规则：

可以构想 \text{Nat} 的效用形如：

Rmk. 这里的 \cong 到目前为止同样是没有正式定义的；暂时可以理解为“自然地效用一致”。

由此在 System F 中这样构造自然数：

接下来是列表类型的邱奇编码，观察列表的消除规则：

类比自然数，可以构想 \text{List}_A 的效用形如：

由此在 System F 中这样构造列表类型：

Rmk. 上面的 head 在严格求值的设定下并不能正常工作；不过无效抽象仍然可以救场。\ Rmk. 这里还假定语言中存在发散项 error，或者说一个 System F 项 \text{error} : \forall T. \ T；尽管原始的 System F 中并没有这样的设定。

有趣的是列表求和函数可以写得非常简洁：

可以想见这是因为我们正是从 iter 出发构造的 \text{CList} 的类型签名。

邱奇编码的一般化 (1) ——归纳类型在 System F 中的表达

与上面的思路一样，我们用 迭代器的类型 编码归纳类型，具体来说就是：

相应的 fold 函数无非是递归类型中介绍的泛型映射的应用：

两种观点

同一全称类型 \forall X. \ T 可以从两个角度理解：

• 逻辑观点：对每一个类型 S 都能给出一个类型为 [X \mapsto S] T 的值。这正是对全称量化 \forall 的直接释读。
• 操作观点：作为一个函数把任意类型 S 映射到其特化项 t \ [S] : [X \mapsto S]T。这正是 \text{E-TAppAbs} 的思路。

基本性质

引理：项代换保持类型

若 \Gamma, x : U \vdash t : T，\Gamma \vdash v : U 且 v 中无自由变量，则 \Gamma \vdash [x \mapsto v] t : T。

Rmk. 在 STLC 中我们往往将 v 的限制写成 \varnothing \vdash v : U，但此处 U 中可能含有 类型变量，因此改成了现在的样子。\ Proof. 对 t 的结构归纳即可。

引理：类型代换保持定型

若 \Gamma, X \vdash t : T 且 \Gamma \vdash T_2 \text{ type}，则 \Gamma \vdash [X \mapsto T_2] t : [X \mapsto T_2] T。

Proof. 对 t 的结构归纳即可。

定理：保持性 (preservation)

若 \Gamma \vdash t : T 且 t \to t'，则 \Gamma \vdash t' : T。

Proof. 对 t \to t' 的结构归纳：

(1) \text{E-AppAbs}, (\lambda x : T_{11}. \ t_{12}) \ v_2 \to [x \mapsto v_2] t_{12}：由 \Gamma \vdash (\lambda x : T_{11} . \ t_{12}) \ v_2 : T 反演得 T = T_{11} \to T_2 且 \Gamma, x : T_{11} \vdash t_{12} : T_2、\Gamma \vdash v_2 : T_{11}，由 项代换保持类型 即证。\ (2) \text{E-TAppAbs}, (\lambda X. \ t_{12}) \ [T_2] \to [X \mapsto T_2] t_{12}：由 \Gamma \vdash (\lambda X. \ t_{12}) \ [T_2] : T 反演得 T = [X \mapsto T_2] T_{12} 且 \Gamma \vdash \lambda X. \ t_{12} : \forall X. \ T_{12}、\Gamma \vdash T_2 \text{ type}，再反演得 \Gamma, X \vdash t_{12} : T_{12}，最后由 类型代换保持定型 即证。\ (3) 剩余的同余情形：对 \Gamma \vdash t : T 反演得到子项的类型，由归纳假设得到约简后的类型，再重组即得。

定理：进展性 (progress)

若 t 为具有类型的闭式，则要么 t 为值，要么存在 t' 使得 t \to t'。

Proof. 对 t 的类型推导归纳：

(1) \text{T-Var}：与空上下文矛盾。\ (2) \text{T-Abs}, \text{T-TAbs}：此时 t 显然为值。\ (3) \text{T-App}, t = t_1 \ t_2：由归纳假设可知 t_1 为值或可约简一步 t_1 \to t_1'，若为后者则可取 t' = t_1' \ t_2；否则反演可得 t_1 = \lambda x : T_{11}. \ t_{12}，由归纳假设亦可知 t_2 为值或可约简一步 t_2 \to t_2'，若为后者则可取 t' = t_1 \ t_2'，否则可取 t' = [x \mapsto t_2] t_{12}。\ (4) \text{T-TApp}, t = t_1 \ [T_2]：由归纳假设可知 t_1 为值或可约简一步 t_1 \to t_1'，若为后者则可取 t' = t_1' \ [T_2]，否则反演可得 t_1 = \lambda X. \ t_{12}，即可取 t' = [X \mapsto T_2] t_{12}。

定理：强约简性 (strong normalization)

若 t 为具有类型的闭项，则 t 求值终止（即经有限步约简会得到值）。

Rmk. 证明较为困难，参见 [3]。

非直谓性 (impredicativity)

回顾一下我们之前提到的 \text{selfApp} = \lambda x : (\forall X. X \to X). \ x \ [\forall X. X \to X] \ x，在 \text{T-TApp} 的调用中，我们将 \forall X. \ X \to X 代入了 \forall X. \ X \to X 的 X 中。

乍一看感觉有点不对？假设 System F 的所有类型“具有类型” \text{Type}，则 (\forall X : \text{Type}. \ X \to X) : \text{Type}……？

这就是说在定义 \text{Type} 中“包含的所有类型”时，全称量词遍历了 \text{Type} —— ？！罗素悖论？！

直观地说，非直谓性就是说 定义里的量词论域允许包含被定义对象本身；与之相反的解决方案就如 Rocq 采取的 类型宇宙 (type universe) 方案：将所有类型划分为可数无穷个类型层级 \text{Set} \ (\text{Type}_0) : \text{Type} \ (\text{Type}_1) : \text{Type}_2 : \cdots，这样构造出的类型系统具有 直谓性 (predicativity)。

Rmk. 不过 Rocq 中的命题类型 \text{Prop} : \text{Type} 是非直谓的，即在定义命题时可以对命题做全称量化，例如：

Definition ex : Prop := forall P : Prop, P -> P.

但与集合论面临的困境不同，很幸运的是 System F 的逻辑是一致的。

定理：一致性 (consistency)

不存在项 t 使得 \varnothing \vdash t : \bot，其中 \bot = \forall X. X。

Proof. 考虑反证法：假设这样的 t 存在，由 强约简性 将其约简为值 v，保持性 指出 \varnothing \vdash v : \bot，可见只能有 v = \lambda X. \ t'，其中 X \vdash t' : X。\ 仍由 强约简性 将其约简为值 v'，保持性 指出 X \vdash v' : X，此时 v' 不能是项变量、不能是 \lambda x : T. \ t''（因为 X 不是箭头类型）、也不能是 \lambda X. \ t''（因为 X 不是全称类型），矛盾！明所欲证。

参数性 (parametricity)

我们在先前邱奇编码的讨论中贯彻了这样一种思想：

• 一个类型（在 System F 中）的定义取决于 它被如何使用。
• 这个定义是 唯一确定的，是 与类型被如何实例化无关的。

最典型的例子譬如 \text{CUnit} “只能”对应于恒等函数，\text{CBool} “只能”对应于两个二选一，以及 \bot 在 System F 中没有闭式。

现在我们来尝试如何表征一个类型的定义是如何 独立于实例化 的，也就是说我们需要考察那些 只与类型自身结构有关 的 性质。

下面三个定义指定了实例化的三个要素——怎么观察行为、类型变量代表什么具体类型、变量代表什么具体项。

定义：可容许性质 (admissible property)

称 P 是类型 T 的一个可容许性质，若 P 对 头展开 (head expansion) 封闭，即若闭项 t : T 使得 t \to t' 且 P(t')，则 P(t)；记作 P : T。

定义：类型替换 (type substitution)

称 \delta 是上下文 \Gamma 的一个类型替换，若 \delta 给每个类型变量 X \in \Gamma 指定了闭类型 \delta(X)，它对 \Gamma \vdash T \text{ type} 给出替换后的结果 \hat{\delta}(T) = [X_1 \mapsto \delta(X_1), \cdots, X_n \mapsto \delta(X_n)] T；记作 \delta : \Gamma。

定义：可容许性质指派 (admissible property assignment)

称 \eta 是类型替换 \delta : \Gamma 的一个可容许性质指派，若 \eta 给每个类型变量 X \in \Gamma 指派了一个可容许性质 \eta(X) : \delta(X)；记作 \eta : \delta。

定义 (基于类型结构的一元关系)

归纳定义关系 t \in T[\eta : \delta] 如下：

(1) t \in X[\eta : \delta] 若 \eta(X)(t)；\ (2) t \in (T_1 \to T_2)[\eta : \delta] 若 \forall t_1 \in T_1[\eta : \delta], t \ t_1 \in T_2[\eta : \delta]；\ (3) t \in (\forall X. \ T)[\eta : \delta] 若 \forall 闭类型 S 和性质 P : S，t \ [S] \in T[(\eta, X : P) : (\delta, X : S)]。

可以想见如此的定义排除了“在代码中判断类型实现专用多态”这样的想法。

定义：项替换 (term substitution)

称 \gamma 是上下文 \Gamma 的一个项替换，若 \gamma 给每个自由变量 x \in \Gamma 指定了闭项 \gamma(x)，它对 \Gamma \vdash t : T 给出替换后的结果 \hat{\gamma}(t) = [x_1 \mapsto \gamma(x_1), \cdots, x_n \mapsto \gamma(x_n)] t；记作 \gamma : \Gamma。\ 进一步地，称 \gamma : \Gamma[\eta : \delta]，若对每个自由变量 x 都有 \gamma(x) \in \Gamma(x)[\eta : \delta]。

定义：语义定型

称 \Gamma \vdash t \in T，若任给 \delta : \Gamma, \eta : \delta, \gamma : \Gamma，只要 \gamma \in \Gamma[\eta : \delta]，就有 \hat{\gamma}(\hat{\delta}(t)) \in T[\eta : \delta]。

此处 \delta, \eta, \gamma 的任意性强调了，类型变量参与的语义 完全由类型决定、与你用什么性质检验无关。

定理：参数性

若 \Gamma \vdash t : T，则 \Gamma \vdash t \in T。

Proof. 对 t 的类型推导归纳即可。

例子：\text{CUnit} (1)

命题：\forall X. \ X \to X 的参数性

设闭项 f : \forall X. \ X \to X，则任给类型 T 和性质 P : T，若闭项 t : T 使得 P(t)，则 P(f \ [T] \ t)。

Proof. 由闭项 f : \forall X. \ X \to X 和 参数性定理 可知 \varnothing \vdash f \in \forall X. \ X \to X，由定义 (3) 可知对于任意性质 P : T，有 f \ [T] \in (X \to X)[(X : P) : (X : T)]。\ 由定义 (1) 可知 t \in X[(X : P) : (X : T)]，再由定义 (2) 可知 f \ [T] \ t \in X[(X : P) : (X : T)]，最后由定义 (1) 即得 P(f \ [T] \ t)。

推论：\forall X. \ X \to X 的唯一性

闭项 f : \forall X. \ X \to X 在 \beta-等价意义下唯一，只可能为 \text{id} = \lambda X. \ \lambda x : X. \ x。

Proof. 由函数的外延性和 System F 的 强约简性，只需证明任给类型 T 和闭项 t : T，都有 f \ [T] \ t =_{\beta} \text{id} \ [T] \ t。\ 定义性质 P = \{t' : T \mid t' =_{\beta} t\}，易见 P 对头展开封闭且 P(t)。\ 由 \forall X. \ X \to X 的参数性 可知 P(f \ [T] \ t)，则 f \ [T] \ t =_{\beta} t = \text{id} \ [T] \ t。明所欲证。

接下来暂时将目光从简单的全称类型 \forall X. \ X \to X 上移开，回顾我们在列表理论中习见的一些等式：

• 已知以下列表上的函数：

• 则有如下法则：

熟悉基础范畴论的读者应当立刻意识到这无非是在说下面的自然性方块成立：

神奇的是你会发现，把 \text{reverse} 换成任何一个具有 \forall X. \ \text{List} \ X \to \text{List} \ X 类型的多态函数——比如 \lambda X. \ \lambda x : \text{List} \ X. \ \text{app} \ x \ (\text{reverse} \ x)、\lambda X. \ \lambda x : \text{List} \ X. \ \text{nil}——我们也有类似的法则成立。

可以想见这是因为对 X 的全称量化限制我们只能“丢弃”或“保留”所输入的列表中的项。

事实上这样的“交换性”的确是成立的，并统称为 免费定理 (theorems for free) ——因为它是由类型而非具体实现给出的。为便研究，下面把参数性从 一元的性质 扩展到 二元的关系：与上面的区别无非是增加一个分量，为完整性起见仍呈现如下。

定义：可容许关系

称 R 是类型对 (T_1, T_2) 的一个可容许关系，若 R 对 双坐标头展开 封闭，即若闭项 t_1 : T_1, t_2 : T_2 使得 t_1 \to t_1', t_2 \to t_2' 且 R(t_1', t_2')，则 R(t_1, t_2)；记作 R : T_1 \times T_2。

定义：类型替换对

称 (\delta_1, \delta_2) 是上下文 \Gamma 的一对类型替换，若 \delta_1, \delta_2 分别给每个类型变量 X \in \Gamma 指定了闭类型 \delta_1(X), \delta_2(X)，它们分别诱导 \hat{\delta}_1(T) 与 \hat{\delta}_2(T)；记作 \delta_1, \delta_2 : \Gamma。

定义：可容许关系指派

称 \eta 是类型替换对 \delta_1, \delta_2 : \Gamma 的一个可容许关系指派，若 \eta 给每个类型变量 X \in \Gamma 指派了一个可容许关系 \eta(X) : \delta_1(X) \times \delta_2(X)；记作 \eta : \delta_1, \delta_2。

定义 (基于类型结构的二元关系)

归纳定义关系 (t_1, t_2) \in T[\eta : \delta_1, \delta_2] 如下：

(1) (t_1, t_2) \in X[\eta : \delta_1, \delta_2] 若 (t_1, t_2) \in \eta(X)；\ (2) (t_1, t_2) \in (T_1 \to T_2)[\eta : \delta_1, \delta_2] 若 \forall (u_1, u_2) \in T_1[\eta : \delta_1, \delta_2], (t_1 \ u_1, t_2 \ u_2) \in T_2[\eta : \delta_1, \delta_2]；\ (3) (t_1, t_2) \in (\forall X. \ T)[\eta : \delta_1, \delta_2] 若 \forall 闭类型对 (S_1, S_2) 和可容许关系 R : S_1 \times S_2，(t_1 \ [S_1], t_2 \ [S_2]) \in T[(\eta, X : R) : (\delta_1, X : S_1), (\delta_2, X : S_2)]。

定义：项替换对及其匹配

称 (\gamma_1, \gamma_2) 是上下文 \Gamma 的一对项替换，若 \gamma_1, \gamma_2 分别给每个自由变量 x \in \Gamma 指定了闭项 \gamma_1(x), \gamma_2(x)，它们分别诱导 \hat{\gamma}_1(t) 与 \hat{\gamma}_2(t)；记作 \gamma_1, \gamma_2 : \Gamma。\ 进一步地，称 \gamma_1, \gamma_2 : \Gamma[\eta : \delta_1, \delta_2]，若对每个自由变量 x 都有 (\gamma_1(x), \gamma_2(x)) \in \Gamma(x)[\eta : \delta_1, \delta_2]。

定义：语义定型（二元 ver.）

称 \Gamma \vdash (t_1, t_2) \in T，若任给 \delta_1, \delta_2 : \Gamma; \eta : \delta_1, \delta_2; \gamma_1, \gamma_2 : \Gamma，只要 \gamma_1, \gamma_2 : \Gamma[\eta : \delta_1, \delta_2]，就有 (\hat{\gamma}_1(\hat{\delta}_1(t_1)), \hat{\gamma}_2(\hat{\delta}_2(t_2))) \in T[\eta : \delta_1, \delta_2]。

定理：参数性（二元 ver.）

若 \Gamma \vdash t : T，则 \Gamma \vdash (t, t) \in T。

Proof. 对 t 的类型推导归纳即可。

例子：\text{CUnit} (2)

命题：\forall X. \ X \to X 的免费定理

设闭项 f : \forall X. \ X \to X，则对任意闭项 g : S \to T 和闭项 t : S，有 f \ [T] \ (g \ t) =_{\beta} g \ (f \ [S] \ t)。\ 或者说下面的自然性方块成立：

\begin{array}{ccc} S & \xrightarrow{g} & T \\ f_S \Big\downarrow & & \Big\downarrow f_T \\ S & \xrightarrow{g} & T \end{array}

Proof. 由闭项 f : \forall X. \ X \to X 和 参数性定理（二元 ver.） 可知 \varnothing \vdash (f, f) \in \forall X. \ X \to X，由定义 (3) 可知对于任意闭类型对 (S_1, S_2) 和可容许关系 R : S_1 \times S_2，有 (f \ [S_1], f \ [S_2]) \in (X \to X)[(X : R) : (X : S_1), (X : S_2)]。\ 定义关系 R = \{(u : S, v : T) \mid v =_{\beta} g \ u\}，易见 R 对双坐标头展开封闭且 R(t, g \ t)。\ 由定义 (1) 可知 (t, g \ t) \in X[(X : R) : (X : S), (X : T)]，再由定义 (2) 可知 (f \ [S] \ t, f \ [T] \ (g \ t)) \in X[(X : R) : (X : S), (X : T)]，最后由定义 (1) 即得 R(f \ [S] \ t, f \ [T] \ (g \ t))，即 f \ [T] \ (g \ t) =_{\beta} g \ (f \ [S] \ t)。明所欲证。

为了对更一般的归纳类型给出其 System F 表示的免费定理，我们先来将一般归纳类型的 邱奇编码 记作：

其中 F \ X “保存了归纳类型的构造方式”，例如 \text{Ind}_{X. \text{Unit} + X} = \forall X. \ ((\text{Unit} + X) \to X) \to X \cong \text{CNat}。

下面来给此处 F 的内涵进行严格的定义。

代数数据类型 (algebraic data types)

用以下的语法定义代数数据类型：

其中 0 即空类型 \bot，1 即单位类型 \text{Unit}，X 为既知类型或类型变量。使用喜闻乐见的 同构递归 记法，我们可以写出如下等式：

……其与 \mu-类型记法之间的转换方式是显然的。

既然定名 代数 数据结构，我们留意到下面的代数性质：

• (1) 加法零元：0 + A \cong A \cong A + 0。
• (2) 加法交换律：A + B \cong B + A。
• (3) 加法结合律：A + (B + C) \cong (A + B) + C。
• (4) 乘法幺元：1 \times A \cong A \cong A \times 1。
• (5) 乘法交换律：A \times B \cong B \times A。
• (6) 乘法结合律：A \times (B \times C) \cong (A \times B) \times C。
• (7) 乘法分配律：A \times (B + C) \cong A \times B + A \times C。
• (8) 零次幂律：A^0 \cong 1。
• (9) 指数对和的分配律 / 解包和类型的两个分支：A^{B + C} \cong A^B \times A^C。
• (10) 指数对积的分配律 / 生成积类型的两个分量：(A \times B)^C \cong A^C \times B^C。
• (11) 幂的乘方律 / 柯里化 (currying)：A^{B \times C} \cong (A^B)^C。

……其中 \cong 被定义为两个类型间存在 双射；同时我们将函数类型 A \to B 视为 幂 B^A，鉴于当 A, B 的 居留者 (inhabitant) 有限时其恰有 |B|^{|A|} 个取值。

Rmk. 严格来说，若不保证 A, B 的居留者都有限时，A \to B 的“有效”取值可能少于 |B|^{|A|}（基数运算），因为并非所有取值都是可计算的。典型的例子如 A = \text{Nat}, B = \text{Bool}，此时 A \to B 相当于 \mathbb{R}，其中绝大多数都是不可计算数。

由此 ADT 在同构意义下 构成 交换半环 (commutative semiring)，并带有一个符合通常性质的幂运算。

F-代数 (F-algebra)

给定范畴 \mathcal{C}，设 F : \mathcal{C} \to \mathcal{C} 为自函子，X \in \text{Ob}(\mathcal{C})，f : F \ X \to X 为态射，则称三元组 \langle F, X, f \rangle 为一个 F-代数；其中称 X 为 载体 (carrier)，f 为 结构映射。

在类型论的语境下，取 \text{Ob}(\mathcal{C}) 为所有闭的代数数据类型，\text{Mor}(\mathcal{C}) 为类型之间的所有函数，现在我们就可以（手动）给定义各个 \text{Ind}_F 时写出的 F 赋予 自函子 的意义了：

• (1) \text{Bool}：对象映射 F \ X = 1 + 1，态射映射 F \ (f : X \to Y) = \text{id}_{1 + 1}。
• (2) \text{Nat}：对象映射 F \ X = 1 + X，态射映射 F \ (f : X \to Y) = \lambda s : 1 + X. \ \text{case } s \text{ of } \text{inl } \text{unit} \Rightarrow \text{inl } \text{unit} \mid \text{inr } x \Rightarrow \text{inr } (f \ x)。
• (3) \text{List}_A：对象映射 F \ X = 1 + A \times X，态射映射 F \ (f : X \to Y) = \lambda s : 1 + A \times X. \ \text{case } s \text{ of } \text{inl } \text{unit} \Rightarrow \text{inl } \text{unit} \mid \text{inr } \{a, x\} \Rightarrow \text{inr } \{a, f \ x\}。

据此对 正类型算子 X.F 写出其对态射 h : S \to T 的作用：

Rmk. 可以发现这里的 \text{map}_F 与我们在讨论递归类型时定义的泛型映射是相似的。

容易验证这样构造的自函子 F 保持单位态射和态射的复合。

当 F 取定，所有 F-代数 \langle F, X, f \rangle 对应的 (X, f) 亦构成 F-代数范畴 F \texttt{-Alg}：我们令 \text{Hom}((X, f), (Y, g)) 包含所有 \mathcal{C} 中这样的态射 h : X \to Y，它使得 h \circ f = g \circ F \ h；或者说下面的自然性方块成立：

称这样的 h 为一个从 \langle F, X, f \rangle 到 \langle F, Y, g \rangle 的 F-代数同态。

在此之上，我们给出免费定理在 F-代数同态背景下的表述。

免费定理（F-代数同态 ver.）

设 X.F \text{ pos}，闭项 c : \text{Ind}_F，则对任意 F-代数同态 h : (A, f_A) \to (B, f_B)，有 h \ (c \ [A] \ f_A) =_{\beta} c \ [B] \ f_B。

Proof. 定义关系 R = \{(u : A, v : B) \mid h \ u =_{\beta} v\}，由 F-代数同态的定义可知 h \circ f_A = f_B \circ F \ h。\ 与 \forall X. \ X \to X 的情形相似，可以通过应用构造子证明 R(c \ [A] \ f_A, c \ [B] \ f_B)，即 h \ (c \ [A] \ f_A) =_{\beta} c \ [B] \ f_B。明所欲证。

可以发现这个自然性方块与 \text{map-reverse swap} 法则的自然性方块是神似的。下面我们开始讨论 F 与对应的递归类型间的关联。

始代数 (initial algebra)

称 F-代数范畴中的始对象为一个始代数，记作 (\mu F, \text{in}_F)。

Rmk. 这里的 \mu F 不是 构造 出来的而是 定义 出来的，请注意与递归类型一讲中的 \mu-类型记法 \mu X. \ F \ X 加以区分；不过后面我们将说明两者确实是等价的。

泛性质指出其若存在则在同构意义下唯一，并且对任意 F-代数 \langle F, X, f \rangle 存在唯一 的 F-代数同态 \text{fold} \ [X] \ f : \mu F \to X。

在类型论的语境下，若将 \text{fold} 视作函数，得到其类型为 \forall X. \ (F \ X \to X) \to \mu F \to X ——神奇的是，这与邱奇编码的类型 \forall X. \ (F \ X \to X) \to X 很相似啊！只是前者多了一个 \mu F 的参数。

下面的定理将宣告始代数 存在 并可用邱奇编码 构造。

定理：邱奇编码为始代数

设 X. F \text{ pos}，则存在 \text{in}_F^{(C)} 使得 (\text{Ind}_F, \text{in}_F^{(C)}) 为始代数。

Proof. 先证存在性。令 \text{fold}^{(C)} \ [X] \ f = \lambda c : \text{Ind}_F. \ c \ [X] \ f，\text{in}_F^{(C)} = \lambda v : F(\text{Ind}_F). \ \lambda X. \ \lambda f : F \ X \to X. \ f \ (F \ (\text{fold}^{(C)} \ [X] \ f) \ v)。\ 任给 F-代数范畴中的对象 (X, f)，欲证自然性方块

\begin{array}{ccc} F \ \text{Ind}_F & \xrightarrow{F \ (\text{fold}^{(C)} \ [X] \ f)} & F \ X \\ \text{in}_F^{(C)} \Big\downarrow & & \Big\downarrow f \\ \text{Ind}_F & \xrightarrow{\text{fold}^{(C)} \ [X] \ f} & X \end{array}

成立，而利用函数的外延性这无非是定义的操演：

\text{fold}^{(C)} \ [X] \ f \ (\text{in}_F^{(C)} \ v) = \text{in}_F^{(C)} \ v \ [X] \ f = f \ (F \ (\text{fold}^{(C)} \ [X] \ f) \ v)

再证唯一性。任给 c : \text{Ind}_F，由 免费定理 可知：

c \ [X] \ f = \text{fold}^{(C)} \ [X] \ f \ (c \ [\text{Ind}_F] \ \text{in}_F^{(C)}) = (c \ [\text{Ind}_F] \ \text{in}_F^{(C)}) \ [X] \ f

由函数的外延性即得 c = c \ [\text{Ind}_F] \ \text{in}_F^{(C)}。设 h : (\text{Ind}_F, \text{in}_F^{(C)}) \to (X, f) 为 F-代数同态，则由 免费定理 可知：

h \ c = h \ (c \ [\text{Ind}_F] \ \text{in}_F^{(C)}) = c \ [X] \ f = \text{fold}^{(C)} \ [X] \ f \ c

由函数的外延性即得 h = \text{fold}^{(C)} \ [X] \ f。明所欲证。

到此我们可以安心地使用 (\mu F, \text{in}_F) 代表始代数了。我们先前曾写下 \text{Nat} \cong 1 + \text{Nat} 这样的同构，而现在我们终于能够严谨地证明它了！

Lambek 定理

设 X. F \text{ pos}，则 \mu F \cong F(\mu F) 且 \text{in}_F 为同构。

Proof. 构造 \text{out}_F = \text{fold}^{(C)} \ [F(\mu F)] \ (F \ \text{in}_F) : \mu F \to F(\mu F)，容易验证 \text{in}_F \circ \text{out}_F = \text{id}_{\mu F}, \text{out}_F \circ \text{in}_F = \text{id}_{F(\mu F)}，故 \mu F \cong F(\mu F) 且 \text{in}_F 为同构。

到此我们已经构建了“邱奇编码为什么是对的”的理论，但同时还有一个问题没有得到解决——为什么邱奇编码是长成 \forall X. \ (F \ X \to X) \to X 这样的？有没有一种不那么 Ad-hoc 的解释？

首先自 [5] 引述范畴论中的经典结果—— 米田引理 (the Yodena lemma)：

取定宇宙 \mathcal{U}，设 \mathcal{C} 为 \mathcal{U}-小范畴，\texttt{Set} 为 \mathcal{U}-集所成范畴。\ 定义协变 米田嵌入 函子：

\begin{aligned} k_{\mathcal{C}} : \mathcal{C} &\to \text{Fct}(\mathcal{C}, \texttt{Set}) \\ S &\mapsto \text{Hom}_{\mathcal{C}}(S, \cdot) \end{aligned}

Rmk. 说人话：函子 k_{\mathcal{C}}(S) 包含了从 S 看出去的所有箭头的信息。

定理：米田引理（协变 ver.）

对于 S \in \text{Ob}(\mathcal{C}) 和 B \in \text{Ob}(\text{Fct}(\mathcal{C}, \texttt{Set}))，映射

\begin{aligned} \text{Nat}(h_S, B) &\to B(S) \\ \left[\text{Hom}_{\mathcal{C}}(S, \cdot) \xrightarrow{\phi} B(\cdot) \right] &\mapsto \phi_S(\mathrm{id}_S) \end{aligned}

为双射，它对 S, B 都是自然的。函子 k_{\mathcal{C}} 是全忠实的。

Rmk. 说人话：一个自然变换 \phi : k_{\mathcal{C}}(S) \to B 完全由它在恒等态射处的值 \phi_S(\text{id}_S) \in B(S) 决定；自然性会将结果输送到其他 X \in \text{Ob}(\mathcal{C})。

值得我们关注的是这样一个思想：

现在取 \mathcal{C} = \texttt{Set}（或者严谨地说，\mathcal{U}-小集所成范畴），B 为恒等函子 \text{id}，由米田引理可知：

现将左边展开，考察自然变换 \eta : \text{Hom}_\mathcal{C}(S, \cdot) \to \text{id} 的分量

……可见这恰与 System F 中的多态函数 \forall X. \ (S \to X) \to X 相对应。于是直观上可以想见：

下面代入几个特例看看：

• (1) 令 S = \text{Unit} = 1，得到 1 \cong \forall X. \ (1 \to X) \to X \cong \forall X. \ X \to X。
• (2) 令 S = \text{Bool} = 1 + 1，得到 1 + 1 \cong \forall X. \ ((1 + 1) \to X) \to X \cong \forall X. \ ((1 \to X) \times (1 \to X)) \to X \cong \forall X. \ (X \times X) \to X \cong \forall X. \ X \to X \to X。

不过令人遗憾的是这只能 解释 非递归类型。为处理递归类型，下面让我们把视角从 \texttt{Set} 换到 F \texttt{-Alg} 上。

改令 \mathcal{C} = F \texttt{-Alg}，B 为遗忘函子 U ——它将 (X, f) 送回类型 X 自身。现取 S 为始代数 (\mu F, \text{in}_F)，由米田引理可知：

始代数的泛性质指出，任给 (X, f) \in \mathcal{C}，\text{Hom}_{\mathcal{C}}((\mu F, \text{in}_F), (X, f)) 均为单点集 \{\text{fold} \ [X] \ f\}，于是自然变换 \eta : \text{Hom}_{\mathcal{C}}((\mu F, \text{in}_F), \cdot) \to U 的分量

无非是说指派一个 X 中的元素。虑及 f : F \ X \to X，我们可以立刻写出类型

……显见具有此类型的项 c 与所有自然变换 \eta 一一对应：只需令 \eta_{(X, f)} : \text{fold} \ [X] \ f \mapsto c \ [X] \ f，而反之亦然。

由此可见，邱奇编码的形式完全可以说是米田引理的结果（尽管这不是证明）：

在此基础上，介绍一些有趣的视角：

(i) 考虑 \eta 在恒等态射处的取值，有 \text{id}_{(\mu F, \text{in}_F)} = \text{fold} \ [\mu F] \ \text{in}_F，在两边应用 c 即导出 c = c \ [\mu_F] \ \text{in}_F。\ (ii) 考虑 \eta 在 F-代数同态 h : (A, f_A) \to (B, f_B) 上的自然性：

\begin{array}{ccc} \{\text{fold} \ [A] \ f_A\} & \xrightarrow{\eta_{(A, f_A)}} & A \\ h_* \Big\downarrow & & \Big\downarrow h \\ \{\text{fold} \ [B] \ f_B\} & \xrightarrow{\eta_{(B, f_B)}} & B \end{array}

这意味着 h \ (c \ [A] \ f_A) = c \ [B] \ f_B，此即免费定理。

存在类型 (Existential Types)

下面来考察一个 余归纳类型 ——流。

就像我们讨论归纳类型的 消除 规则一样，现在观察流的 生成 规则：

留意到参数类型 S 并不会出现在结论之中，这就是说我们应当将其视作一种“内部状态”——例如递归类型一讲中我们介绍的 \text{from0}（内部状态是 \text{Nat}）和 \text{fib}（内部状态是 \text{Nat} \times \text{Nat}）。

但生成规则的形式并不关心 S 到底是什么：我们只需知道它 存在。

以上的讨论奠定了存在类型的直觉：类型 \exists X. T 就是说存在一个类型 S，使得项具有类型 [X \mapsto S] T；但这个 S 像余归纳类型的生成器一样被 存在量化 “隐藏”起来了，只有一个 \forall S 的项可以将其“消化”。

形式化

1. 语法形式

2. 类型规则

Rmk. 其中 \text{T-Unpack} 的 \Gamma \vdash T_2 \text{ type} 确保了我们所“能够带走”的信息不包含 X。

3. 计算规则

两种观点

同一存在类型 \exists X. \ T 同样可以从两个角度理解：

• 逻辑观点：是以某个类型 S 对应的以 [X \mapsto S] T 为类型的项。
• 操作观点：是某个类型 S 和以 [X \mapsto S] T 为类型的项组成的对。

下面我们主要采取操作观点，略举两例：

• (1) e_1 = \{^* \text{Nat}, \{0, \lambda x : \text{Nat}. \ \text{succ} \ x\}\} \text{ as } \{\exists X, X \times (X \to X)\}。
• (2) e_2 = \{^* \text{Bool}, \{\text{tru}, \lambda x : \text{Bool}. \ \text{fls}\}\} \text{ as } \{\exists X, X \times (X \to X)\}。

可以发现 e_1, e_2 具有同一类型 \{\exists X, X \times (X \to X)\}，但其内部的 X 却是 不同 的！

——这就是说，如果有人想要 消除 一个存在类型，他就需要能够对 任意 一个 X 都能够处理对应的项！

邱奇编码举隅 (2)

现在回到流这个简单的余归纳类型：我们消除它无非是为了生成某个类型 Y 的项，这就需要能处理 任意 隐藏状态类型 S 的生成器 g，它接受流初始化的状态和流的步进、生成目标类型的项。

上面的观察已经提供了这样一种直觉：g 可以被编码为 全称类型

——因此考虑在 System F 中这样构造 \text{Stream}_A 类型：

邱奇编码的一般化 (2) ——余归纳类型在 System F 中的表达

推而广之，我们用 生成器的类型 编码余归纳类型，具体来说就是：

相应的 unfold 函数同样是递归类型中介绍的泛型映射的应用：

抽象数据结构 (abstract data types, ADTs)

存在类型的一个经典应用是抽象数据结构。一个 ADT 包含：

(1) 一个抽象类型的名称 A；\ (2) 一个具体的表示类型 T；\ (3) 实现的若干对 A 的操作（如创建、修改、查询）；\ (4) 一堵禁止外界访问 T 的“墙”。\ Rmk. (4) 指的是外界只能调用你实现的这些 抽象 的操作，而不能获知 T 具体 是什么、亦不能直接对其进行操作；另一种理解则是 T 的 作用域 仅在你实现这些操作的场域内。

下面使用存在类型编码 ADT。以计数器为例：

一件有趣的事情是，我们还可以实现各种各样不同的计数器……？

……尽管这看上去非常没有道理；我们甚至可以写出更多的“计数器”，并会发现只要其内部实现类型正确，无论你调用哪一个计数器，原本类型正确的外部实现依然是类型正确的。尽管结果显然可能有问题。

——这正是一个 参数性 的应用！在访问者看来，T 相当于被全称量化了，与之相关的合法操作仅限于该 ADT 暴露的操作。因此外部实现的类型是否正确完全取决于其自身和 ADT 的 类型声明，而与 ADT 的 内部实现 无关。

Rmk. 这与软件工程中的 模块 (module) 和 包 (package) 的概念有异曲同工之妙！我们同样可以选择只向使用者暴露哪些接口。

存在对象 (existential objects)

在 ADT 之外，存在类型的另一个经典应用是 纯函数式 风格的对象的构造。其核心思想为：

当需要改变对象的内部状态时，我们不去修改它，而是构建一个新的对象。

仍以计数器为例。一个计数器对象由：(1) 一个数（其内部状态 state）；(ii) 一对方法（其外部接口 methods）构成：

可见对象与 ADT 的结构几乎一致，不同的则是语义：对象的抽象类型是由状态和方法两个字段组成的整个存在类型，而 ADT 的抽象类型是其中的 \exists \text{Counter}。

这样说可能有些奇怪，下面举一个简单的例子：

• 对于计数器 ADT 而言，

let {Counter, counter} = newCounterADT in
  counter.inc(counter.new) as Counter

• 得到的就是一个新的 ADT，但对于对象 c : \text{Counter} 而言，

let {X, body} = c in
  body.methods.inc(body.state)

• 却会抛出作用域异常：究其原因，body.methods.inc(body.state) 的类型 X 的作用域仅限于这个 let-in 表达式内部，尝试将其向上返回不符合 \text{T-Unpack} 的要求。
• 一个合法的实现需要重新打包：

let {X, body} = c in
  {*X,
   {state = body.methods.inc(body.state),
    methods = body.methods}}
  as Counter

而当问题从一元操作升级到二元运算，对象的问题将凸显出来。考虑实现一个自然数集合的数据结构，其内部实现是平衡树，而我们不希望将其暴露在外：

• 构造自然数集合 ADT：

• 再来尝试构造自然数集合对象：

• 对前者而言，只需使用 let {Counter, counter} = newCounterADT in ... 打开一个包含 \text{Counter} 的作用域，随后可以在其中任意取用 union 等方法。
• 但对后者而言，我们无法直接对两个 NatSet 对象使用 union 方法：因为其内部封装的 \exists X 不一定相同——或者说“参数性”所致——！
• 为使其类型正确，一个可能的方案是将 union 的类型签名改为

• ……但这样做还是有两个问题：(i) 需要引入递归类型；(ii) 这实则是将前面的问题一股脑抛给了 union 的实现、它仍不能访问第二个参数的具体结构。

存在类型在 System F 中的表达

当我们使用 let-in 表达式消费一个存在类型时即引入 参数 X 和 \Gamma, X \vdash t : T，最终产出了一个新的类型 S，因此可以在 System F 中这样表达存在类型：

两条类型规则分别对应：

Rmk. 可以体会一下 \forall 和 \exists 的“对偶性”！

在此基础上，可以还原出存在类型消除的计算规则：

Rmk. 事实上我们早就用上了这个编码！在推导流的邱奇编码时，我们将生成器 g 设想为内含状态 S 的状态机

\{\exists X, X \times (X \to A \times X)\} = \forall Y. \ (\forall S. \ S \times (S \to A \times S) \to Y) \to Y \cong \text{CStream}_A

——这无非是存在类型在 System F 中的表达！

Reference

• [1] 北京大学 2026 年春《编程语言的设计原理》中 Variable Types 一讲的 slides。
• [2] Types and Programming Languages, Chapter 23 Universal Types & Chapter 24 Existential Types。
• [3] Proofs and Types, Chapter 14 Strong Normalisation for F。
• [4] Church Encoding, Parametricity, and the Yoneda Lemma。
• [5] 《代数学方法（第一卷） 基础架构》，第二章《范畴论基础》。