第七章二阶类型系统：多态与抽象

阅读提示

本章会频繁使用 ∀X.T、∃X.T、ΛX.t、t[T]、参数化多态（parametric polymorphism）、存在类型（existential type）、类型算子（type operator）等术语。若你在阅读时想快速回查定义与记号，建议配合：

附录A《术语表》中的 A.5“多态、二阶系统与抽象相关术语”

附录B《符号速查表》中的“类型系统相关记号”“容易混淆的符号对照”

第六章的一阶类型系统已经能够描述很多常见的数据结构：布尔值、自然数、积类型、和类型、记录、递归类型、引用类型等。但它仍然有一个明显限制：

它只能谈“具体类型”，还不能自然表达“对任意类型都成立”的程序。

例如，恒等函数应该不只适用于 Bool，也不只适用于 Nat。我们真正想表达的是：

它对布尔值可用；
对自然数也可用；
对任意类型的值都可用。

这就引出本章的主题：二阶类型系统（second-order type system）。

这里的“二阶”主要是指：

类型系统中不仅有“项变量”；
还允许对“类型变量”进行抽象和应用；
因而可以在类型层面表达多态与抽象。

本章要回答的问题是：

为什么一阶系统不够；
System F 如何表达参数化多态；
存在类型如何表达“隐藏实现、暴露接口”；
为什么类型算子会把我们进一步带向更高阶的类型层结构。

同时要先固定一个边界：

本章前半的核心对象是 System F（也叫二阶 Lambda 演算），重点讨论显式的全称多态；后半的存在类型与类型算子，则更适合看作围绕这条主线展开的典型扩展与延伸。

因此，本章的重点是建立这些概念的直觉和最基本形式，而不是完整覆盖所有高阶类型理论细节。尤其是存在类型和类型算子部分，会以“够用的形式化 + 清晰的直觉”来呈现；更深入的 kind、Fω 等主题，只做方向性介绍。

如果你之后要读第 9 章，也请先记住一个重要区分：

本章讨论的是显式写进对象语言的多态构造；第 9 章讨论的则是 HM 路线中更受限但更易自动推断的多态机制。两者相关，但不是同一个系统。

7.1 为什么需要二阶类型系统？

先看一个在前面章节里已经很熟悉的函数：恒等函数。

在带类型注解的一阶系统里，我们可以写：

$λ x : Bool . x : Bool \to Bool$

也可以写：

$λ x : Nat . x : Nat \to Nat$

这两个函数当然都叫“恒等函数”，但在一阶系统里，它们是两个不同的项：

一个作用于 Bool
一个作用于 Nat

问题在于：
我们缺少一个统一表达，来说明“这其实是同一种程序模式，只不过适用于任意类型”。

也就是说，一阶系统缺少一种能力：

对类型本身做抽象。

而这正是参数化多态的核心思想。

7.1.1 两种“多态”直觉

在进入形式系统之前，先区分两种常见直觉：

参数化多态：程序对“任意类型”都以统一方式工作；
特设多态：程序根据不同类型采取不同实现方式。

本章讲的是第一种，即参数化多态。
它的典型特征是：

程序不会“检查当前类型到底是什么”；
而是对所有类型一视同仁地工作。

例如恒等函数：

不关心输入是布尔值还是自然数；
它只是把输入原样返回。

这正是参数化多态最纯粹的例子。

7.2 System F：最经典的参数化多态系统

表达参数化多态的经典形式系统是 System F，也叫二阶 Lambda 演算（second-order lambda calculus）。

它在普通 Lambda 演算的基础上，多加入了两类构造：

类型抽象（type abstraction）
类型应用（type application）

可以把它和普通函数抽象做一个平行类比：

值层面	类型层面
$λ x . t$	$Λ X . t$
$t_{1} t_{2}$	$t [T]$

直觉上：

$λ x . t$ ：对“值”抽象
$Λ X . t$ ：对“类型”抽象

以及：

$t_{1} t_{2}$ ：把函数应用到一个值
$t [T]$ ：把多态项应用到一个类型

这里先特别提醒一个后文会反复用到的边界：

在本章里，∀X.T、ΛX.t、t[T] 都是对象语言的一部分；也就是说，它们不是讲解时临时使用的元语言记号，而是 System F 本身的正式构造。

这点和第 9 章会出现的 HM 类型方案（type scheme）非常不同。到那时你会看到：虽然两边都会写出某种 ∀，但它们所在的层级并不相同。

7.2.1 类型与项的扩展语法

System F 在类型层面增加：

$T ::= \dots ∣ X ∣ \forall X . T$

其中：

$X$ 是类型变量
$\forall X . T$ 表示“对任意类型 $X$ ，类型 $T$ 成立”

在项层面增加：

$t ::= \dots ∣ Λ X . t ∣ t [T]$

其中：

$Λ X . t$ 是类型抽象
$t [T]$ 是类型应用

7.2.2 `∀X.T` 的直觉

类型

$\forall X . T$

读作：

对任意类型 $X$ ，都有一个 $T$ 类型的程序。

例如：

$\forall X . X \to X$

表示：

一个程序，对任意类型 $X$ ，都能接受一个 $X$ 类型的值，并返回一个 $X$ 类型的值。

这正是“多态恒等函数”的类型。

7.3 参数化多态的最基本例子：多态恒等函数

现在可以正式写出多态恒等函数：

$Λ X . λ x : X . x$

它的类型是：

$\forall X . X \to X$

这比前面的一阶版本更强，因为它不是某个具体类型上的恒等函数，而是：

对任意类型都成立的恒等函数。

7.3.1 如何使用它？

要把多态函数用于某个具体类型，需要做一次类型应用。

例如，如果记：

$i d = Λ X . λ x : X . x$

那么：

$i d [Bool] : Bool \to Bool$

以及：

$i d [Nat] : Nat \to Nat$

更进一步：

$i d [Bool] true ⟶ true$

$i d [Nat] 0 ⟶ 0$

它的使用过程和普通函数应用完全平行：

先把多态项实例化为某个具体类型；
再把普通值传给它。

7.3.2 这和“一阶里写两个恒等函数”有什么不同？

一阶系统里，我们只能分别写：

Bool -> Bool 版本
Nat -> Nat 版本
其他类型再写其他版本

而 System F 里，我们写出的是一个统一的项：

$Λ X . λ x : X . x$

它明确表达了：

这个程序模式本身是统一的；
只是当你真正使用时，才把其中的类型变量实例化成具体类型。

这就是参数化多态的本质。

7.4 System F 的基本类型规则

为了让前面的写法不只是直觉，我们还需要给出最基本的类型规则。

7.4.1 类型抽象规则

$\frac{Γ , X ⊢ t : T}{Γ ⊢ Λ X . t : \forall X . T} (T-TAbs)$

它的意思是：

在环境中加入类型变量 $X$
如果项 $t$ 的类型是 $T$
那么类型抽象 $Λ X . t$ 的类型就是 $\forall X . T$

这里需要补一个记号层面的说明。
在第五章里，我们把 $Γ$ 介绍成“项变量到类型的有限映射”；而到了 System F，这个记号通常会被略作扩展，用来同时记录：

项变量的类型假设；
当前可用的类型变量。

因此这里的 $\Gamma, X$ 最稳妥的理解是：

在原有项变量上下文的基础上，额外假定类型变量 X 处于作用域中。

有些教材会把这两类信息拆成两个上下文分别书写，例如把“类型变量上下文”和“项变量上下文”分开；本章为了保持记号简洁，继续沿用同一个 $\Gamma$ ，但你应当记住它在这里的含义比第五章稍宽。

可以把它类比成普通函数抽象：

普通函数抽象：假设一个值变量，再构造函数体
类型抽象：假设一个类型变量，再构造项

也就是说，从这一章开始，Γ 不再只是“变量到类型的映射”，而是一个同时承载项变量假设与类型变量作用域信息的上下文。

7.4.2 类型应用规则

$\frac{Γ ⊢ t : \forall X . T}{Γ ⊢ t [ T ^{'} ] : [ X \mapsto T ^{'} ] T} (T-TApp)$

它的意思是：

如果 $t$ 是一个对任意类型都成立的多态项；
那么就可以把其中的类型变量 $X$ 用某个具体类型 $T^{'}$ 替换掉；
从而得到实例化后的类型。

这里的 $[X \mapsto T^{'}] T$ 是类型层面的替换。
它和第三章项层面的替换在形式上很像，但对象不同：

第三章替换的是项中的变量；
这里替换的是类型中的类型变量。

7.4.3 一个完整的类型推导直觉

对于：

$Λ X . λ x : X . x$

可以这样理解它的类型推导：

假设类型变量 $X$ 可用；
在此基础上，判断 $λ x : X . x$ 的类型；
显然它的类型是 $X \to X$ ；
因此整个项的类型是：

$\forall X . X \to X$

这个过程本质上就是：

先在类型层面引入一个“任意类型”的占位符，再在其下构造一个普通函数。

7.5 参数化多态到底提供了什么？

如果只看恒等函数，参数化多态好像只是“少写几遍类型”。但它的意义远不止于此。

这里也可以顺手和第 9 章先做一个对照：

本章讨论的是显式写出的参数化多态；
第 9 章讨论的是 HM 路线中可自动推断的 let-多态。

前者表达力更强，后者更易算法化。理解这条分界线，会让后面读 HM 时轻松很多。

7.5.1 统一表达“对任意类型成立的程序”

例如下面这些程序模式都天然是多态的：

恒等函数
常函数
函数组合
把一个函数应用到一个值
在不检查具体类型的前提下重新组织数据

这些程序共同点在于：

它们的行为不依赖于具体类型的内部结构。

7.5.2 支持抽象与复用

参数化多态让我们可以写出真正可复用的程序，而不是为每种类型重复造轮子。

例如“一对相同类型值”的构造函数，就可以统一写成某种多态形式，而不必分别为：

Bool
Nat
String
记录类型
列表类型

都单独写一个版本。

7.5.3 与“只靠类型别名复用”不同

要注意，参数化多态不是简单的“类型写少一点”。
它是一种真正的表达能力增强，因为它允许类型变量进入程序结构，并在使用时被实例化。

7.6 参数化多态与真实语言中的泛型

System F 常被当作现代泛型与参数化多态语言的理论原型。

7.6.1 直觉对应

例如，许多语言或伪代码里都会有类似“恒等函数”的写法：

identity x = x

这类例子能帮助你抓住一个很弱但有用的直觉：

这个函数看起来不依赖输入的具体类型细节；
它只是把输入原样返回。

而在类型理论里，System F 给了这种直觉一个明确的形式：

$\forall X . X \to X$

不过这里要特别保持边界感。
如果你拿动态语言里的函数来做类比，它只能帮助你理解“同一段程序代码似乎能处理多种值”这一点，却不能直接等同于参数化多态。因为在动态语言里，函数往往仍然可以：

检查运行时值的种类；
根据不同输入走不同分支；
利用运行时信息改变行为。

而真正的参数化多态直觉更强调：

程序对所有类型以统一方式工作，而不是在运行时窥探“当前到底是什么类型”。

7.6.2 与真实语言并不完全一样

不过要保持边界感。
现实语言中的泛型机制并不一定就是完整的 System F；而动态语言里“一个函数能处理多种值”这件事，也不应直接被说成参数化多态本身。

更稳妥的说法是：

System F 提供了参数化多态的一个经典理论核心；
某些静态语言中的泛型、某些动态语言里“统一处理多种值”的经验直觉，都能帮助你从不同角度靠近这个主题；
但真实语言通常还会加入额外特性，例如：
- 类型擦除
- 约束
- 类型类
- 特化
- 推断
- 运行时类型信息

因此，不能简单说：

“某门语言的泛型系统就是 System F。”

或者

“动态语言里一个看起来通用的函数，就已经等于参数化多态。”

更准确的说法是：

System F 是理解参数化多态的重要理论模型。

7.6.3 关于 Zig 的类比

如果要把本章内容和 Zig 联系起来，最稳妥的说法是：

Zig 也支持把“类型”作为编译期参数参与程序构造；
但它的机制与 System F 中的纯粹类型量化并不完全相同；
因而更适合作为“相关设计”的比较对象，而不是“直接等价物”。

也就是说：

Zig 中的编译期类型参数可以帮助你建立“程序对多种类型适用”的直觉，但它不应被直接当成 System F 的字面实现。

7.7 System F 的一个重要边界：推断并不总是容易

从第五章到现在，我们一直使用显式类型注解。
这是有意为之，因为一旦进入多态系统，很多事情会立刻变得更微妙。

一个重要事实是：

在显式注解的 Church 风格下，System F 的类型检查是可以讨论和实现的；
但在不带注解的 Curry 风格下，完整的 System F 类型推断并不像 Hindley–Milner 那样简单。

这里最好把边界说得再硬一点：

System F 允许你在对象语言里显式写出 ∀X.T、ΛX.t、t[T]；
HM 则主要允许在 let 绑定处得到可泛化的类型方案（type scheme）；
因而第 9 章不是在讲“如何自动推断本章完整系统”，而是在讲一条表达力更受限、但更适合自动推断的路线。

本章不展开这些技术细节，只先记住一条主线：

System F 擅长表达参数化多态
但“如何自动推断出这些类型”是另一回事

这也是为什么现实语言常常在“表达力”和“可推断性”之间做取舍。第九章讲 Hindley–Milner 时，这条线索会重新出现。

7.8 存在类型：隐藏实现，只暴露接口

从这一节开始，本章会稍微离开“最小 System F 核心”，转而讨论围绕二阶多态展开的一个典型扩展：存在类型（existential type）。

也就是说，下面的内容仍然和本章主线紧密相关，但你最好把它理解成：

围绕显式多态展开的抽象机制扩展，而不是“前面最小 System F 核心的唯一继续写法”。

前面讲的全称类型

$\forall X . T$

表达的是：

对任意类型都成立。

而现在要讲的存在类型

$\exists X . T$

表达的是：

存在某个类型 $X$ ，使得 $T$ 成立。

这两个量词虽然都作用在类型变量上，但直觉完全不同。

7.8.1 `∀` 与 `∃` 的区别

$\forall X . T$ ：强调统一适用于所有类型
$\exists X . T$ ：强调隐藏某个具体类型，只暴露其接口

可以把存在类型理解成一种“打包”机制：

包里确实有一个具体实现类型；
但包的使用者看不到它究竟是什么；
使用者只能通过给定接口操作它。

这正是数据抽象最核心的思想。

7.9 一个存在类型的例子：抽象计数器

考虑这样一种抽象对象：

它能创建一个计数器状态；
能读取当前值；
能得到递增后的新状态。

我们可以写成：

$\exists C . {new : C, get : C \to Nat, inc : C \to C}$

这里的直觉是：

C 是内部状态类型；
但外部用户并不知道 C 到底是什么；
用户只知道有一组操作围绕这个隐藏类型工作。

这个 C 可能是：

一个自然数；
一个更复杂的记录；
某种编码后的结构；

但这些实现细节都被隐藏起来了。

于是存在类型表达的是：

我不告诉你内部表示类型是什么，但我保证有这样一组接口。

这和很多现实语言里的“抽象数据类型”思想非常接近。

7.10 存在类型的基本直觉规则

为了让“隐藏实现”这件事更形式化，存在类型通常配套两种操作：

打包（pack）
拆包（unpack）

虽然本章不把完整规则系统展开到所有细节，但至少要理解这两步的角色。为了让直觉更稳，这里先给出一个最小规则形状。

一种常见写法是：

打包： $pack [S, t] as \exists X . T$
拆包： $unpack [X, x] = t_{1} in t_{2}$

它们的直觉分别是：

pack：选定某个具体实现类型 S，再把对应实现值 t 封装进存在类型；
unpack：临时打开这个包，在 t_2 中把隐藏类型当作抽象的 X、把对应实现值当作 x 来使用。

这里最重要的不是记住完整形式细节，而是抓住一条作用域纪律：

拆包之后，你只能把隐藏类型当作一个抽象占位符来使用，而不能依赖它的真实实现身份。

7.10.1 打包

打包做的事情是：

选定某个具体类型 $S$ ；
构造一个使用该类型实现的值；
把它封装成某个存在类型。

直觉上类似于：

“这里有一个实现，它确实满足接口，但我不把实现类型直接告诉你。”

7.10.2 拆包

拆包做的事情是：

打开一个存在类型包；
临时拿到“隐藏类型变量”和对应值；
但之后只能按照接口使用它，不能依赖其真实实现类型。

直觉上类似于：

“我现在知道这里有个内部类型占位符，但我依然不能假装知道它具体是什么。”

7.10.3 为什么需要拆包规则限制？

因为如果拆包后你能随便窥探实现类型，那“抽象”就失效了。
存在类型的关键不是“里面有东西”，而是：

里面的具体实现必须被隐藏。

也正因此，存在类型通常被看作：

模块系统
抽象数据类型
接口与实现分离

的一个理论原型。

7.11 参数化多态与存在类型的关系

这两个概念经常一起出现，因为它们共同构成了“抽象”的两个方向。

7.11.1 参数化多态：对使用者统一

参数化多态表达的是：

不管你给我什么类型，我都按统一方式工作。

它强调的是泛化与统一行为。

7.11.2 存在类型：对实现者隐藏

存在类型表达的是：

我这里有某种实现，但我不把实现细节暴露给你。

它强调的是封装与隐藏表示。

这两者结合起来，就得到了数据抽象最经典的两面：

一方面，程序可以对任意类型编写通用逻辑；
另一方面，实现细节可以被包起来，只暴露必要接口。

因此，更稳妥的结论是：

参数化多态与存在类型共同构成了类型化抽象的重要基础。

而不是说它们“已经完整等于所有模块系统”——真实语言的模块机制通常还会包含更多东西。

7.12 类型算子：从二阶多态走向更高阶类型层结构

到目前为止，我们已经允许：

类型变量出现在类型里；
用量词对类型变量进行抽象。

再往前一步，一个自然问题是：

能不能像写函数那样，写“从类型到类型”的构造？

这就引出类型算子（type operator）。

这里要先明确一个边界：

类型算子已经不再只是“最小 System F 核心里的另一个普通构造”。它更像是从二阶多态继续向前走时，自然会遇到的类型层抽象扩展。

因此，本节的目标不是把完整更高阶系统讲完，而是帮助你建立一个稳定直觉：类型本身也可以像函数参数那样被组织、抽象和复用。

7.12.1 直觉

类型算子可以理解成：

以类型为输入，产生新类型的“类型层函数”。

例如，一个“二元组构造器”可以直觉写成：

$Pair = λ X . λY . X \times Y$

那么：

$Pair [Bool] [Nat]$

就对应于：

$Bool \times Nat$

这里要注意：

这已经不是普通项层面的 Lambda；
而是发生在类型层面的抽象与应用。

7.12.2 为什么它重要？

因为很多类型构造其实都带有“可参数化”的性质。例如：

列表类型构造器
结果类型构造器
映射类型构造器
某些模块签名中的类型模板

如果没有类型算子，我们只能得到很多具体展开后的类型；
有了类型算子，就可以把这些“类型模式”本身抽象出来。

7.13 关于类型算子的边界：为什么会引出更高阶系统？

一旦允许类型算子，就会出现新的问题：

哪些“类型层函数”是合法的？
类型算子的参数自己又是什么“种类”？
怎样区分“普通类型”和“从类型到类型的构造器”？

这就会引出 kind（种类）系统，以及更高阶的类型理论，例如 System Fω。

也就是说，到这里为止，本章已经从：

一阶系统中“只能谈具体类型”
走到 System F 中“可以显式量化类型变量”
再走到“可以抽象生成类型的方式”

这条线索说明：类型层面的抽象能力会一层层增强，而每增强一层，系统边界与形式化负担也会随之上升。

但对本章来说，你只需要先抓住一个最核心的认识：

类型算子让我们不仅能使用类型，还能抽象“生成类型的方式”。

这已经足以帮助你理解为什么“类型层面的抽象能力”会比一阶系统强得多。

7.14 本章小结

这一章引入了从一阶类型系统走向二阶类型系统的三个关键概念。

7.14.1 参数化多态

通过全称量化：

$\forall X . T$

我们可以表达：

一个程序对任意类型都成立；
它的行为不依赖于具体类型的内部结构。

这正是 System F 最核心的内容。

7.14.2 存在类型

通过存在量化：

$\exists X . T$

我们可以表达：

某个实现类型确实存在；
但它被隐藏起来；
外部只能通过接口使用它。

这提供了抽象数据类型的核心直觉。

7.14.3 类型算子

通过类型层面的抽象与应用，我们可以把：

“某个具体类型”
推进为
“一个生成类型的模式”

从而把类型本身也变成可组织、可抽象的对象。

7.14.4 如果压缩成一句话

本章最重要的一句话是：

二阶类型系统让我们不仅能给项分类，还能对类型本身做抽象。

这使得类型系统的表达力一下子扩大了很多：

可以表达真正的参数化多态；
可以表达隐藏实现的数据抽象；
还可以进一步走向类型层面的函数与高阶结构。

同时，也要记住本章内部的层次差别：

System F 是本章前半的显式多态核心；
存在类型是围绕这条主线展开的重要抽象扩展；
类型算子则把我们进一步带向更高阶的类型层结构。

如果把本章和第 9 章放在一起看，最值得记住的分界是：

本章强调显式写进对象语言的多态表达力；第 9 章强调更受限但更易自动推断的 HM 路线。

回看导航

如果你读完本章后，想把“二阶类型系统”重新挂回全书主线，最推荐的回看顺序是：

回看第 6 章：重新确认一阶系统为什么只能处理“具体类型”，从而看清本章为什么必须引入“对类型本身的抽象”。
回看附录A：重点查看“参数化多态”“System F”“全称类型”“存在类型”“打包 / 拆包”“类型算子”“kind / 种类”等条目。
回看附录B：重点确认 ∀X.T、∃X.T、ΛX.t、t[T] 这些记号，以及它们和普通项层构造 λx.t、t1 t2 的对应关系。
若你之后继续读第 9 章，务必先把本章和 HM 路线做一个对照：
- 本章强调更强的显式多态表达力；
- 第 9 章强调更受限但更易自动推断的多态系统。
如果你在阅读第 9 章时开始把“对象语言中的 ∀X.T”和“环境中的类型方案 ∀α.T”混在一起，也建议立刻回到本章 7.2、7.4、7.7 重新确认这条分界线。

本章练习

解释为什么一阶类型系统无法自然表达“对任意类型都成立的恒等函数”。
写出多态恒等函数的 System F 项，并说明它为什么具有类型： $\forall X . X \to X$
比较 $\forall X . X \to X$ 与 $\exists X . X \to X$ 的直觉区别。
用自然语言解释为什么存在类型可以表达“隐藏实现、暴露接口”。
说明“类型算子”与“普通函数”的平行关系：它们分别作用在什么层面？

下一章，我们将继续扩展类型系统的表达能力，但方向会发生变化：

不再主要讨论“对任意类型的抽象”，而是讨论“一个类型能否安全地替代另一个类型”。

这就进入了子类型。

Keyboard shortcuts

编程语言理论与类型系统入门