第5章：多态类型（Polymorphic Types）Polymorphic Types — Universal Types

一、导读

1.1 学习目标

多态是类型系统中最强大的特性之一。本章讲解参数多态（parametric polymorphism），即泛型编程的类型理论基础。通过本章的学习，读者将达成以下目标：

• 掌握 System F（多态 lambda 演算）的语法和类型规则
• 理解类型抽象和类型应用的操作语义
• 掌握 Church 编码在 System F 中的推广——用多态类型编码所有代数数据类型
• 理解参数多态的"参数性"（parametricity）及其带来的免费定理
• 认识 System F 与 STLC 的表达能力差异

1.2 重要性

参数多态是现代编程语言中泛型编程的理论基础。Java 的泛型、C# 的泛型、Haskell 的参数多态、Rust 的泛型——所有这些特性都可以追溯到 System F。System F 由 Jean-Yves Girard 在 1972 年提出（用于证明分析），John Reynolds 在 1974 年独立发现（用于编程语言设计），是类型理论中最重要的系统之一。

参数多态的核心思想是：函数或数据类型可以参数化类型，使得同一份代码能对所有类型统一工作。与子类型多态不同，参数多态不依赖类型之间的层次关系，而是通过类型抽象实现真正的通用性。这种通用性还带来了"免费定理"（Free Theorems）——仅从类型签名就能推导出程序必须满足的性质。

1.3 核心问题

• 参数多态和子类型多态有什么本质区别？
• System F 比 STLC 强大在哪里？它仍然保证终止性吗？
• 如何用多态类型编码列表、树等递归数据结构？
• 什么是"参数性"？为什么仅从类型签名就能推导出程序的行为约束？
• System F 的类型推断是否可判定？

二、核心概念详解

2.1 System F 的语法

System F 在 STLC 的基础上增加了类型变量和全称量词类型。其语法分为类型层和项层两部分：

类型语法：

T ::= α                    -- 类型变量
    | T → T                -- 箭头类型
    | ∀α. T                -- 全称类型（多态类型）

项语法：

e ::= x                    -- 变量
    | λx:T. e              -- 值抽象（普通函数）
    | e e                  -- 值应用（普通应用）
    | Λα. e                -- 类型抽象（多态函数）
    | e [T]                -- 类型应用（实例化多态函数）

类型抽象 Λα. e 创建了一个对类型 α 参数化的多态函数。类型应用 e [T] 将具体类型 T 应用到多态函数，替换其类型参数。这两个操作在类型层面类似于值层面的 lambda 抽象和应用。

2.2 类型规则

System F 的类型判断规则在 STLC 的基础上增加了两条新规则：

类型抽象规则（T-TAbs）：

Γ ⊢ e : T
-------------------------
Γ ⊢ Λα. e : ∀α. T

如果 e 具有类型 T（T 中可能包含自由类型变量 α），则 Λα.e 具有类型 ∀α. T。

类型应用规则（T-TApp）：

Γ ⊢ e : ∀α. T1
-------------------------
Γ ⊢ e [T2] : T1[α := T2]

如果 e 具有多态类型 ∀α. T1，则 e [T2] 的类型是将 T1 中所有自由出现的 α 替换为 T2。

经典的例子是恒等函数：id = Λα. λx:α. x，其类型为 ∀α. α → α。使用时通过类型应用实例化：id [Nat] 的类型为 Nat → Nat，id [Bool] 的类型为 Bool → Bool。

2.3 Church 编码的推广

在 System F 中，Church 编码获得了更强大的表达能力。利用多态类型，可以编码所有代数数据类型（积类型、和类型、列表、树等）。

积类型（Pair）编码：

Pair = ∀α. (A → B → α) → α
pair = ΛA.ΛB.λa:A.λb:B.Λα.λf:A→B→α. f a b
fst = ΛA.ΛB.λp:Pair A B. p [A] (λa:A.λb:B. a)
snd = ΛA.ΛB.λp:Pair A B. p [B] (λa:A.λb:B. b)

和类型（Either）编码：

Either = ∀α. (A → α) → (B → α) → α
inl = ΛA.ΛB.λa:A.Λα.λf:A→α.λg:B→α. f a
inr = ΛA.ΛB.λb:B.Λα.λf:A→α.λg:B→α. g b
case = ΛA.ΛB.λα.λe:Either A B.λf:A→α.λg:B→α. e [α] f g

自然数（Scott 编码的变体）：

Nat = ∀α. (α → α) → α → α
zero = Λα.λs:α→α.λz:α. z
succ = λn:Nat.Λα.λs:α→α.λz:α. s (n [α] s z)

列表编码：

List A = ∀α. (A → α → α) → α → α
nil = ΛA.Λα.λc:A→α→α.λn:α. n
cons = ΛA.λh:A.λt:List A.Λα.λc:A→α→α.λn:α. c h (t [α] c n)

这些编码证明了 System F 可以表达所有代数数据类型，尽管它不支持递归类型。

2.4 参数性与免费定理

参数性（Parametricity）是参数多态最深刻的性质。Reynolds 提出的参数性原理指出：多态函数对其类型参数必须是"统一的"——它不能根据类型参数的具体结构做出不同的行为。一个类型为 ∀α. α → α 的函数必须对所有类型 α 执行相同的操作。

参数性的直接推论是"免费定理"（Free Theorems）：仅从类型签名就能推导出多态函数必须满足的性质。

例如，对于 f : ∀α. α → α，免费定理告诉我们：对所有类型 A 和所有 x : A，f [A] x = x。即 f 必须是恒等函数。因为 f 无法知道 α 是什么类型，它唯一能做的就是把输入原样返回。

再如，对于 f : ∀α.∀β. α → β → α，免费定理告诉我们：f 必须返回第一个参数，忽略第二个参数。因为 f 无法构造 β 类型的值（它不知道 β 是什么），也无法将 α 转换为 β。

又如，对于 map : ∀α.∀β. (α → β) → List α → List β，免费定理告诉我们：map f (map g xs) = map (f ∘ g) xs（融合定律）。这个性质不需要看 map 的实现就能从类型推导出来！

2.5 System F 的性质

System F 具有以下重要的元理论性质：

强规范化：与 STLC 一样，System F 中所有良类型项都保证终止。Girard 证明了 System F 的强规范化定理，这比 STLC 的证明复杂得多，需要使用可归约性候选的推广版本。

类型擦除：System F 的多态类型在运行时可以完全擦除。类型抽象 Λα.e 擦除后就是 e，类型应用 e [T] 擦除后就是 e。这意味着参数多态在运行时没有开销——这是 Java 泛型类型擦除的理论基础。

类型推断不可判定：与 STLC 的扩展 HM 系统不同，System F 的类型推断是不可判定的。不存在通用算法能从无标注的项中推导出 System F 类型。这就是为什么 Haskell 要求对多态函数提供类型签名（或局部类型签名）。

Curry-Howard 对应：System F 对应二阶直觉主义命题逻辑（Second-order Intuitionistic Propositional Logic）。全称类型 ∀α. T 对应二阶全称量词 ∀α. P(α)。这个对应使得 System F 不仅是一个编程模型，还是一个强大的逻辑系统。

三、深入分析

3.1 参数多态 vs 特设多态 vs 子类型多态

多态（polymorphism，意为"多种形态"）在编程中有三种主要形式：

参数多态（Parametric Polymorphism）：函数对所有类型统一工作，不依赖类型的具体结构。如 id : ∀α. α → α。优点是通用性强、可以推导免费定理、运行时零开销。缺点是无法根据类型执行不同操作。

特设多态（Ad-hoc Polymorphism）：函数对不同类型执行不同操作。如 Haskell 的类型类（Type Class）、C++ 的函数重载、Python 的运算符重载。Haskell 的 + 对整数做加法、对浮点数做浮点加法、对字符串做拼接。类型类（如 Eq、Ord、Show）是特设多态的类型安全实现。

子类型多态（Subtype Polymorphism）：函数对类型层次中的不同子类型执行不同操作。如面向对象的虚方法调用。animal.speak() 根据 animal 的实际类型（Dog、Cat 等）调用不同的实现。

三种多态可以组合使用。Scala 同时支持参数多态（泛型类）、特设多态（implicits）和子类型多态（继承）。Rust 的 trait 系统结合了参数多态和特设多态的优点。

3.2 System F 的表达能力

System F 比 STLC 强大得多，但仍然不是图灵完备的（因为强规范化保证了终止性）。System F 可以表达的能力包括：

• 所有 STLC 可表达的函数
• 所有代数数据类型（积、和、列表、树）
• 所有可以用有限迭代表达的计算（通过 Church 编码自然数）
• 高阶函数如 map、fold、filter 的多态版本

System F 不能表达的能力：

• 一般递归（因为强规范化）
• 递归类型（如 μX. 1 + X 表示的自然数类型）
• 自解释器（System F 不能解释自身，这是一个深刻的不可定义性结果）

要获得通用计算能力，需要添加不动点组合子 fix : ∀α. (α → α) → α，但这会破坏强规范化。

3.3 类型擦除与运行时表示

System F 的类型擦除性质对编程语言实现有重要影响。类型擦除意味着多态函数在运行时只有一份代码——id [Nat] 和 id [Bool] 在运行时是同一个函数。这带来了显著的优化空间：

• 多态函数不需要为每种类型实例化一份代码
• 类型信息不占用运行时空间
• 多态调用没有额外的运行时开销

Java 的泛型实现采用了类型擦除策略（出于向后兼容的考虑），这与 System F 的擦除语义一致。但也带来了限制：无法在运行时获取泛型类型参数（instanceof List<String> 不合法），无法创建泛型数组（new T[10] 不合法）。

相比之下，C# 的泛型采用具体化（reification）策略，在运行时保留类型参数信息。这提供了更大的灵活性（支持运行时类型检查），但需要为每种类型实例化一份代码，增加了内存占用。

四、实践案例

4.1 案例一：Haskell 的参数多态

Haskell 是参数多态的典型代表。Haskell 的多态函数遵循参数性原则，使得免费定理成为可能。

-- 类型签名：forall a. [a] -> [a]
-- 免费定理：f (map g xs) = map g (f xs)
-- 即 f 不能改变元素的顺序或数量，只能删除或保留元素
reverse :: [a] -> [a]  -- 违反上述定理，所以 reverse 不是这个定理的候选

-- 类型签名：forall a. [a] -> Int
-- 免费定理：对任何列表，结果只与列表长度有关
-- 因为函数无法检查元素内容（不知道 a 是什么）
length :: [a] -> Int

-- 类型签名：forall a b. (a -> b) -> [a] -> [b]
-- 免费定理：f g (map h xs) = map g (f (map h xs))
-- 即 f 必须逐个处理元素，不能合并或分裂
map :: (a -> b) -> [a] -> [b]

Haskell 社区利用免费定理来推导程序变换和优化。例如，fold/build 融合规则就是基于参数性推导出来的：foldr k z (build g) = g k z。这个规则允许编译器消除中间列表，显著提升性能。

4.2 案例二：Rust 的泛型与单态化

Rust 的泛型系统基于参数多态，但采用了与类型擦除不同的实现策略——单态化（Monomorphization）。编译器为每个具体类型生成一份专用代码：

fn identity<T>(x: T) -> T { x }

// 编译器为每个使用的类型生成专用版本：
// fn identity_i32(x: i32) -> i32 { x }
// fn identity_string(x: String) -> String { x }

单态化的优点是运行时零开销（没有类型擦除后的装箱/拆箱），性能等同于手写专用代码。缺点是代码膨胀——每种使用的类型都生成一份代码，可能增加二进制大小和编译时间。

Rust 还提供了 trait 对象（dyn Trait）作为运行时多态的替代方案，类似于子类型多态。trait 对象使用虚表（vtable）在运行时分发方法调用，提供了灵活性但引入了运行时开销。

五、常见误区

5.1 误区一：泛型就是参数多态

泛型（Generics）是参数多态在编程语言中的实现，但不同语言的泛型可能包含非参数多态的特性。例如 Java 的泛型包含通配符（涉及子类型关系），C++ 的模板包含特化和 SFINAE（涉及特设多态）。真正的参数多态要求函数对所有类型统一工作，不能根据类型执行不同操作。

5.2 误区二：类型擦除意味着类型信息完全丢失

类型擦除只影响运行时表示，不影响编译期检查。在编译期，类型信息完整保留用于类型检查。此外，某些语言通过反射 API 在运行时保留了部分泛型类型信息（如 Java 的 TypeToken 模式、TypeScript 的装饰器元数据）。

5.3 误区三：System F 可以表达所有计算

System F 不是图灵完备的。强规范化定理保证了所有 System F 程序都终止。要表达通用计算，需要添加不动点组合子或一般递归机制，但这会失去终止性保证。

5.4 误区四：免费定理不需要证明

免费定理是从类型签名自动推导出来的，但它们的有效性依赖于参数性假设。如果程序使用了 seq（Haskell）、类型case（模式匹配类型）、或反射等打破参数性的特性，免费定理可能不成立。在使用免费定理进行程序变换时，必须确认程序确实满足参数性。

六、本章小结

本章系统讲解了参数多态和 System F 的核心概念。System F 通过在 STLC 基础上增加类型变量和全称量词类型，实现了参数多态——函数可以对所有类型统一工作。类型抽象和类型应用是类型层面的 lambda 抽象和应用，它们使得多态函数的定义和实例化成为可能。

Church 编码在 System F 中获得了更强大的表达能力，可以编码所有代数数据类型。参数性原理揭示了多态函数的深层约束——仅从类型签名就能推导出程序必须满足的性质（免费定理），这是参数多态独有的优美性质。

System F 保持了强规范化性质（所有程序都终止），但类型推断变得不可判定。类型擦除性质使得参数多态在运行时零开销，对语言实现有重要指导意义。理解 System F 对于深入掌握泛型编程、理解函数式语言的高级特性以及进行形式化验证都具有关键价值。

七、思考题

请写出 System F 中具有类型 ∀α.∀β. α × β → β × α 的项（交换积类型的两个分量）。它的免费定理是什么？

证明在 System F 中，类型为 ∀α. α → α 的唯一闭合项（在 beta-eta 等价意义下）是恒等函数 Λα. λx:α. x。

请用 System F 的 Church 编码实现列表的 map 函数和 foldr 函数，并验证 map f (foldr f z xs) 的融合性质。

研究 Haskell 的 newtype 机制。它和 System F 的类型抽象有什么关系？为什么 newtype 在运行时是零开销的？

System F 的类型推断不可判定，但实际语言（如 Haskell）是如何处理这个问题的？它使用了哪些限制或启发式方法来使类型推断在实践中可行？