第八章子类型

阅读提示

本章会频繁使用 S <: T、T-Sub、协变、逆变、不变等术语。若你一时记不清它们的定义或记号，可随时回查：

附录A《术语表》中的 A.6“子类型与变化方向相关术语”；

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

同时，本章直接依赖：

第 5 章中的类型判断 Γ ⊢ t : T 与类型安全主线；

第 6 章中的记录类型与可变引用。

前几章介绍的类型系统，默认都带着一个很强的假设：

一个项如果被判断为某个类型，那它通常就只能按这个类型来使用。

但在实际编程里，我们经常希望允许一种更灵活的情况：

如果一个值“比要求的还具体”，能不能把它当成“更一般”的值来用？
如果一个记录拥有比你要求更多的字段，能不能把它交给只关心其中一部分字段的代码？
如果一个函数返回更精确的结果，它能不能代替返回较一般结果的函数？

这类问题的统一答案，就是子类型（subtyping）。

本章默认讨论的是结构子类型（structural subtyping）语境。也就是说：

我们主要关心类型结构本身如何决定可替换性；
尤其以记录类型和函数类型为核心例子；
不把“类继承”“名义类型（nominal typing）”“运行时对象模型”直接当作本章的正式对象。

这一章的主线非常明确：

子类型的直觉是安全替换；
形式上我们写作 $S <: T$ ；
真正关键的地方在于：子类型不仅是类型之间的关系，还会进入类型规则本身；
尤其是函数类型的子类型方向，最容易出错。

8.1 子类型的直觉：安全替换

如果 $S <: T$ ，我们读作：

类型 $S$ 是类型 $T$ 的子类型。

它最自然的直觉解释是：

任何一个需要 $T$ 的地方，都可以安全地放入一个 $S$ 。

这通常也被叫做安全替换原则，它和面向对象文献里的里氏替换原则有很强的亲缘关系。

8.1.1 一个最直观的例子：记录

设有两个记录类型：

${nam e : String, a g e : Nat}$

和

${nam e : String}$

直觉上，前者“信息更多”，后者“要求更少”。如果某段代码只需要一个带 name 字段的记录，那么一个同时带 name 和 age 的记录当然也可以拿来用。

因此我们希望有：

${nam e : String, a g e : Nat} <: {nam e : String}$

这就是子类型最朴素的来源：

更丰富的数据
可以被当成更贫瘠的接口来使用

8.2 子类型关系本身：最基本的性质

子类型首先是一个关系。和前面章节中的等价关系、归约关系一样，我们先要说明它具有什么结构性质。

通常，子类型关系至少要求满足：

自反性

$T <: T (S-Refl)$

任何类型都是自己的子类型。

传递性

$\frac{S <: U U <: T}{S <: T} (S-Trans)$

如果 $S$ 可以安全替换为 $U$ ，而 $U$ 又可以安全替换为 $T$ ，那么 $S$ 当然也可以安全替换为 $T$ 。

因此，子类型关系通常至少形成一个前序：

自反
传递

这里要注意一个小边界：

子类型关系不一定是偏序，因为不同类型有时可能彼此可替换却不一定在语法上相同。

不过在本章大多数例子里，把它先理解成“可安全替换关系”就足够了。

8.3 subsumption：子类型为什么会进入类型规则？

如果只给出 $S <: T$ 这样的关系定义，而不把它接入类型判断系统，那么子类型其实还没有真正发挥作用。

真正让子类型“活起来”的规则是 subsumption（包含、提升）规则：

$\frac{Γ ⊢ t : S S <: T}{Γ ⊢ t : T} (T-Sub)$

这条规则的意思是：

如果一个项本来已经有类型 $S$
且 $S$ 是 $T$ 的子类型
那么我们就可以把这个项提升为类型 $T$

这正是“安全替换”在类型系统中的正式入口。

如果你对 subsumption 这个词还不熟，建议同时回看附录A中的对应条目；它和本章的主线几乎是同一个问题的两种表述。

8.3.1 为什么这条规则是主线？

很多初学者第一次学子类型时，会把注意力全部放在“哪些类型彼此有子类型关系”。这当然重要，但还不是核心。

真正的主线是：

子类型之所以重要，是因为它允许我们在类型判断里把“更具体的类型”当成“更一般的类型”来使用。

没有 T-Sub，你就只有“一个抽象的关系”；
有了 T-Sub，这个关系才能真正影响程序是否良类型。

8.4 记录子类型：最容易理解的一类

记录子类型是整个章节里最直观的一类。

8.4.1 宽度子类型化（width subtyping）

如果一个记录拥有更多字段，它可以被当成只要求其中部分字段的记录来使用：

${ l _{i} : T _{i} } ^{i \in 1.. n + k} <: { l _{i} : T _{i} } ^{i \in 1.. n} (S-RcdWidth)$

这条规则表达的是：

左边字段更多
右边字段更少
左边可以看成右边的子类型

直觉上：

需要得少的地方，可以接受给得更多的值。

例如：

${nam e : String, a g e : Nat} <: {nam e : String}$

如果某段代码只要求一个类型为

${nam e : String}$

的记录，那么它只会读取 name 字段；这时你给它一个同时带有 name 和 age 的记录，并不会破坏任何事情。也就是说：

调用方只要求 name
实际值除了 name 之外还额外带了 age
这些额外信息不会妨碍原本只依赖 name 的代码

这正是宽度子类型化最核心的直觉。

8.4.2 深度子类型化（depth subtyping）

如果记录的字段一一对应，而字段类型本身存在子类型关系，那么整个记录也可以形成子类型关系：

$\frac{S _{1} <: T _{1} \dots S _{n} <: T _{n}}{{ l _{1} : S _{1} , \dots , l _{n} : S _{n} } <: { l _{1} : T _{1} , \dots , l _{n} : T _{n} }} (S-RcdDepth)$

这条规则的意思是：

同样的字段名
更具体的字段类型
可以形成更具体的记录类型

8.4.3 宽度与深度可以组合

因此，在复杂一点的记录类型里，你往往会同时用到：

宽度子类型化：字段更多
深度子类型化：字段类型更具体
传递性：把多步推导串起来

这也是为什么 S-Trans 虽然看起来只是“关系论里的常规规则”，但在实际推导中非常有用。

这里还值得补一个小边界：如果把记录理解成“按字段名索引的结构”，那么字段顺序通常不重要；也就是说，我们更自然地把记录看成：

一组带标签的字段；
而不是单纯按位置排列的序列。

因此，本章讨论记录子类型时，默认采用的也是这种按字段名决定结构的视角。

8.5 函数子类型：本章最容易出错的地方

现在进入本章真正的难点：函数类型的子类型。

设我们要比较两个函数类型：

$S_{1} \to S_{2} 和 T_{1} \to T_{2}$

哪一种情况下，前者应该是后者的子类型？

正确规则是：

$\frac{T _{1} <: S _{1} S _{2} <: T _{2}}{S _{1} \to S _{2} <: T _{1} \to T _{2}} (S-Arrow)$

这条规则非常重要，必须认真看清方向。

8.6 为什么函数参数要逆变，返回值要协变？

先分别看两个部分。

8.6.1 返回值：协变

函数返回值的方向最自然。

如果一个上下文期待得到类型 $T_{2}$ 的结果，而你实际提供的函数返回的是更具体的 $S_{2}$ ，且：

$S_{2} <: T_{2}$

那么这是安全的。

因为：

调用者只要求“给我一个 $T_{2}$ ”
你实际给了一个“更具体的 $S_{2}$ ”
这当然没问题

所以函数返回值是协变的。

8.6.2 参数：逆变

函数参数的方向最反直觉，也最关键。

如果一个上下文期待的是函数类型：

$T_{1} \to T_{2}$

这意味着：

上下文可能拿一个 $T_{1}$ 类型的参数来调用这个函数

那么你想拿来替代它的函数，至少必须能接受所有这些 $T_{1}$ 类型的输入。

因此，这个替代函数的参数类型不能比 $T_{1}$ 更窄；它必须至少一样宽，甚至更宽。形式上就是：

$T_{1} <: S_{1}$

也就是：

期待的参数类型在左
实际函数的参数类型在右
方向反过来

所以函数参数是逆变的。

8.7 一个具体例子：为什么参数不能协变？

这是整个章节里最值得真正想清楚的一个反例。

设：

$C a t <: A nima l$

现在假设我们错误地认为函数参数可以协变。那我们就会允许：

$C a t \to C a t <: A nima l \to C a t$

也就是说：

一个“只会处理猫”的函数
可以被当成“能处理任意动物”的函数

这显然不安全。

为什么？

因为如果某段代码拿到了一个类型为 $A nima l \to C a t$ 的函数，它就有权传入任意 Animal，例如一只狗 Dog。
但那个实际函数只能接受 Cat，于是就出问题了。

因此，参数协变会破坏类型安全。

这个反例几乎就是逆变规则最经典的解释：

如果你允许一个“只接受更窄参数”的函数去代替“应当接受更宽参数”的函数，那么调用者迟早会传入一个它处理不了的值。

8.8 重新读一遍函数子类型规则

现在再看一次：

$\frac{T _{1} <: S _{1} S _{2} <: T _{2}}{S _{1} \to S _{2} <: T _{1} \to T _{2}} (S-Arrow)$

你可以这样记：

参数逆变：左看期待，右看实际
结果协变：实际结果可以更具体

也可以记成一句话：

一个函数若想充当另一个函数，就必须“收得更宽，给得更窄（更具体）”。

更精确一点说：

“收得更宽”指参数类型更一般
“给得更具体”指返回类型更具体

8.9 把子类型接回类型规则：应用并不需要改写

有些教材会直接把应用规则改成“带子类型版本”，例如：

$\frac{Γ ⊢ t _{1} : T _{11} \to T _{12} Γ ⊢ t _{2} : T _{21} T _{21} <: T _{11}}{Γ ⊢ t _{1} t _{2} : T _{12}}$

这当然表达了正确直觉，但从结构上说，更清楚的做法通常是：

保持原本的 App 规则不变： $\frac{Γ ⊢ t _{1} : T _{1} \to T _{2} Γ ⊢ t _{2} : T _{1}}{Γ ⊢ t _{1} t _{2} : T _{2}} (T-App)$
再通过 T-Sub 去完成“把更具体类型提升为更一般类型”的工作。

这样做的好处是主线更清楚：

App 仍然只是“函数应用必须参数匹配”
子类型的灵活性来自 T-Sub
整个系统更模块化

不过这里也要补一个实现层面的边界：

这种写法在说明性上最清楚，但在真正设计算法化的类型检查过程时，很多系统还会进一步把规则改写成更语法制导（syntax-directed）的形式。

也就是说，本节的重点首先是把概念结构讲清楚，而不是直接给出某个工业编译器会采用的最终检查算法。

8.9.1 一个简单示意

如果你有：

$Γ ⊢ t_{2} : S 且 S <: T_{1}$

那么由 T-Sub 可以得到：

$Γ ⊢ t_{2} : T_{1}$

这时就能把 t_2 用到要求 T_1 的 T-App 规则中。

所以本章真正的结构主线不是“到处把规则改写成带 <: 的版本”，而是：

先定义子类型关系，再通过 subsumption 让它服务于普通的类型规则。

8.10 其他常见类型构造的变化方向

函数是最难的一类。其他常见构造的方向通常更直观一些。

类型构造	常见变化方向	直觉
函数参数	逆变	必须接受至少和期待一样宽的输入
函数返回值	协变	可以返回更具体的结果
记录宽度	协变	字段更多的记录可替代字段更少的记录
记录深度	协变	字段类型更具体时整体更具体
积类型	通常协变	两边都更具体时整体更具体
和类型	通常协变	两边都更具体时整体更具体

这里的“通常协变”应理解为：

在最常见、纯的、没有额外可变性干扰的设定下；
这些构造往往会沿着“组成部分更具体，则整体更具体”的方向变化。

不过这里要立刻补一个边界提醒：

变化方向并不是“看上去顺眼就行”，而是必须由安全替换原则来论证。

尤其在带可变状态的系统中，某些本来直观看似协变的构造，最后可能必须变成不变。

8.11 为什么可变引用通常是不变的？

虽然本章还没有正式展开引用子类型，但这是一个非常重要的现象，值得在这里先建立直觉。

设你有引用类型：

$R e f (T)$

它既可以：

被读取（读出一个 $T$ ）
又可以被写入（写入一个 $T$ ）

如果你让它协变，就会在“写入”时出问题；
如果你让它逆变，就会在“读取”时出问题。

因此，引用类型通常必须是不变的（invariance）。

这也是一个非常有代表性的模式：

一个既出现在“输出位置”又出现在“输入位置”的类型构造，往往不能简单协变或逆变。

这一点其实已经和第六章的可变引用形成呼应：在那里我们引入了 Ref(T) 及其读写操作，而一旦再把子类型加进来，就会立刻遇到“读取想要协变、写入想要逆变”的张力。

因此，更准确地说：

可变引用之所以通常取不变，不只是一个孤立结论，而是第六章“状态”与本章“变化方向”交叉后的自然结果。

如果你需要回忆引用类型、解引用、赋值和存储类型的基本背景，可以先回看第六章对应小节，再回来看这里的“不变性”会更顺。进一步说，一旦把子类型真正接入带存储的系统，类型安全证明也必须同时跟踪：

项本身的类型；
存储位置中允许放入什么类型；
以及这些位置在读写过程中不会因为错误的变化方向而被破坏。

这也是为什么“引用不变”不仅是一个局部技巧，而是和整个带状态系统的安全性直接相关。

8.12 子类型与类型安全

现在把这一章和第五章连起来。

第五章告诉我们：

类型系统的目标，是保证良类型程序不会掉进坏状态；
这通常通过进展性和保持性来表达。

引入子类型以后，这个目标并没有改变。变化在于：

项不再只有一个“完全精确”的使用方式；
一个更具体的值可以被提升为更一般的类型；
因此保持性和相关引理中，需要把子类型关系考虑进去。

直观上，这不会破坏安全性，因为：

T-Sub 只允许安全提升
<: 关系本身就是按“安全替换”设计的

所以，子类型并不是“放松类型系统导致不安全”，而是：

在不牺牲安全性的前提下，给类型系统增加更灵活的可用性。

当然，前提是你真的把变化方向写对了。
这也是为什么 S-Arrow 的方向一旦写反，整个系统的安全直觉就会崩掉。

8.13 与真实语言的类比：应当怎样说才稳妥？

很多现实语言里都能看到子类型的影子，但类比时最好保持克制。

可以安全类比的地方

记录宽度子类型化，直觉上接近“只关心部分字段的接口”
某些面向对象语言中的“子类可在父类位置使用”，在非常粗略的层面上接近子类型思想
方法参数与返回值的变化方向，和函数子类型有深刻关系
第六章里记录类型与引用类型提供了本章最直接的前置背景：前者帮助理解记录子类型，后者帮助理解为什么某些构造不能自由协变

不应说得太满的地方

真实语言的对象系统不等于“记录 + 子类型”
类继承不等于语义上完美的子类型
真实语言往往还涉及可变状态、方法重写、名义类型、运行时机制等额外因素

因此，更稳妥的说法是：

子类型提供了一套形式化框架，帮助我们理解很多真实语言中的“更具体类型可在更一般位置使用”的现象。

而不是说“某语言的对象系统就是这里的子类型系统”。

换句话说，本章和真实语言之间最适合建立的是：

结构上的类比；
安全替换直觉上的类比；
而不是“逐个语言特性逐字对应”的类比。

8.14 本章小结

这一章的真正主线可以压缩成四句话：

子类型的直觉是安全替换：
$S <: T$
表示任何需要 $T$ 的地方，都可以安全地使用 $S$ 。
subsumption 规则是真正把子类型接入类型系统的关键： $\frac{Γ ⊢ t : S S <: T}{Γ ⊢ t : T}$
记录子类型最容易理解：字段更多、字段更具体，都可能带来子类型关系。
函数子类型最容易出错，但也最重要：
- 参数逆变
- 返回值协变

也就是说，正确的函数子类型规则是：

$\frac{T _{1} <: S _{1} S _{2} <: T _{2}}{S _{1} \to S _{2} <: T _{1} \to T _{2}} (S-Arrow)$

如果你读完这一章，只记住一个技术点，那就应该是：

函数参数逆变，返回值协变，而这一切都必须服从安全替换原则。

若你之后在阅读第九章类型推断时，发现自己一时把“类型相等约束”和“子类型关系”混在一起了，也可以回到本章重新确认：
HM 风格推断的主线主要处理“相等 / 合一”，而本章处理的是“可安全提升”的 <: 关系，这两者相关，但不是同一个问题。

回看导航

如果你读完本章后，想把这一章重新挂回全书主线，最推荐的回看顺序是：

回看第 6 章：重新确认记录类型与引用类型的直觉，因为它们分别对应本章中最典型的记录子类型与不变性讨论。
回看第 5 章：重新确认类型判断、类型安全、进展性与保持性，因为本章的“安全替换”最终仍然服务于“良类型程序不会落入坏状态”这条主线。
回看附录A：重点查看“子类型”“安全替换”“subsumption”“协变”“逆变”“不变”等条目。
回看附录B：重点确认 S <: T、T-Sub、函数类型箭头 T_1 \to T_2 与归约箭头 \longrightarrow 的区别。
若你准备继续读第 9 章，也可以先把本章和“类型相等 / 合一”刻意区分开来：本章处理的是“可安全提升”，而不是“必须相等”。

本章向后输出的核心内容是：

S <: T 作为安全替换关系的读法；
T-Sub 如何把子类型真正接入类型判断；
协变、逆变、不变这三种变化方向的基本直觉；
为什么函数参数逆变、返回值协变，以及为什么引用通常取不变。

本章练习

解释为什么下面的子类型关系成立： ${nam e : String, a g e : Nat} <: {nam e : String}$
说明为什么 T-Sub 是子类型系统的主线，而不是一个“可有可无的补丁规则”。
给出一个具体反例，说明如果函数参数按协变处理，会产生什么类型安全问题。
设有： $C a t <: A nima l$ 判断下面哪个子类型关系应当成立，并说明理由：
- $C a t \to C a t <: A nima l \to A nima l$
- $A nima l \to C a t <: C a t \to A nima l$
- $A nima l \to C a t <: A nima l \to A nima l$
用自然语言解释为什么引用类型通常不能简单协变或逆变。

下一章我们将进入另一个非常重要的问题：

如果程序里没有显式写出所有类型注解，编译器如何自动推断出类型？

这就引出类型推断与合一算法。

Keyboard shortcuts

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