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

第六章 一阶类型系统：基本类型构造

阅读提示

本章会频繁使用“基础类型（base type）”“积类型（product type）”“和类型（sum type）”“记录类型（record type）”“递归类型（recursive type）”“引用类型（reference type）”等术语。若你在阅读时想快速回查定义与记号，建议配合：

• 附录A《术语表》中的 A.4“一阶类型构造相关术语”
• 附录B《符号速查表》中的“类型系统相关记号”

同时，本章直接建立在第 5 章的类型判断 Γ ⊢ t : T 之上；若你对“类型规则”“语法制导”“类型安全”的基本骨架还不稳，建议先回看第 5 章。

第五章建立了简单类型 Lambda 演算（STLC）的最小核心：变量、函数抽象、函数应用，以及最基本的类型判断与类型安全性质。但如果只停留在函数类型，语言的表达能力仍然非常有限——我们还不能自然地表示布尔值、数字、二元组、记录、列表、树，甚至也还没有办法讨论可变存储。

这一章的任务，就是在 STLC 的基础上逐步加入这些更接近真实语言的类型构造。

这里说的一阶类型系统（first-order type system），主要是指：

• 还没有引入对类型本身的量化（如 $\forall X.T$、$\exists X.T$）；
• 因而还没有进入参数化多态或存在类型；
• 但已经可以表达很多常见的数据结构与程序构造。

换句话说，这一章研究的是：

在不引入“类型层面的抽象与量化”之前，一个类型系统能扩展到什么程度？

在阅读本章时，还需要先固定一个形式化层级上的约定：

本章的重点是建立一阶类型构造的统一直觉与最小规则骨架，而不是把所有扩展都写成同一精度的完整形式系统。

更具体地说：

• 基础类型、积类型、引用类型会给出较直接的规则形状；
• 和类型会同时提示“教学上的简写”和“更严格的 Church 风格写法”之间的区别；
• 记录类型会以最小形式骨架为主，为第 8 章的结构子类型做准备；
• 递归类型会明确采用同构递归（iso-recursive）视角，而不是把递归展开直接并入类型相等。

本章既延续第 5 章“类型规则如何工作”的主线，也为第 7–10 章埋下几个关键伏笔：

• 第 7 章会继续讨论“对类型本身做抽象”；
• 第 8 章会回到记录与引用，讨论子类型与变化方向；
• 第 10 章则会进一步讨论：类型不仅描述“值是什么”，还描述“值怎样被使用”。

6.1 为什么要超出函数类型？

在 STLC 中，最核心的类型构造是函数类型：

$$T_1\to T_2$$

这当然很重要，因为函数是整个类型理论的核心对象。但如果一个语言只有函数类型，就会立刻遇到很多实际问题：

• 我们如何表示“真 / 假”？
• 如何表示“两个值的组合”？
• 如何表示“要么是这个，要么是那个”？
• 如何定义列表、树这样的递归结构？
• 如何讨论带状态的程序？

因此，从 STLC 走向更实际的类型系统，第一步通常不是“先加高级多态”，而是先加入这些最基本的数据构造。

这一章会按下面的顺序展开：

1. 基础类型
2. 积类型
3. 和类型
4. 记录类型
5. 递归类型
6. 可变引用

这些构造虽然看起来彼此分散，但它们背后有一条清晰主线：

类型系统不仅要给函数分类，还要给程序中出现的各种数据形态分类。

6.2 基础类型

最自然的扩展，是加入一些“原子性的”基础类型（base types），例如布尔值、自然数和单位类型。

6.2.1 基础类型的直觉

在 STLC 里，函数类型告诉我们：

• 一个项如果类型是 $T_1\to T_2$，
• 那么它应该接收一个 $T_1$ 类型的输入，
• 并产生一个 $T_2$ 类型的结果。

但现实程序里还有很多根本不是“函数”的值，例如：

• true、false
• 0、1、2
• “什么信息都不携带，只表示操作完成了”的值

因此，常见的一阶类型系统通常会引入如下基础类型：

其中最容易误解的是 Unit。
它不是“空值”，而是“恰好只有一个值的类型”。

你可以把它理解成：

• 这个值本身不携带有趣信息；
• 但“返回了一个 Unit 值”仍然是一件事情。

这和很多语言中的“过程调用完成了，但没有返回有用结果”的情况很接近。

6.2.2 一个简单的布尔系统

如果给 STLC 加上布尔值和条件表达式，可以得到如下语法扩展：

$$\begin{array}{rl}T& ::=\dots \mid \text{Bool}\\ t& ::=\dots \mid \text{true}\mid \text{false}\mid \text{if }{t}_1\text{ then }{t}_2\text{ else }{t}_3\end{array}$$

相应的类型规则是：

$$\frac{}{\Gamma ⊢\text{true}:\text{Bool}}\text{(T-True)}$$

$$\frac{}{\Gamma ⊢\text{false}:\text{Bool}}\text{(T-False)}$$

$$\frac{\Gamma ⊢t_1:\text{Bool}\Gamma ⊢t_2:T\Gamma ⊢t_3:T}{\Gamma ⊢\text{if }{t}_1\text{ then }{t}_2\text{ else }{t}_3:T}\text{(T-If)}$$

这里最重要的是 if 的规则：

• 条件部分必须是 Bool；
• 两个分支必须有相同类型；
• 整个 if 表达式的类型就是这个共同类型。

这条规则体现了一个非常典型的类型系统思想：

表达式的类型必须在运行前就能确定，而不能取决于运行时到底走了哪个分支。

如果你读到这里时，想快速确认 Bool、Nat、Unit、类型判断 Γ ⊢ t : T 等记号的含义，也可以顺手回查附录A和附录B中的对应条目。

6.2.3 关于 Nat 与机器整数

理论里的 Nat 一般表示数学意义上的自然数。
它和真实语言里的 int、i32、u64 并不完全一样。

更准确地说：

• Nat 常被用作一个理想化的、无限的自然数类型；
• 而真实语言里的机器整数通常是有位宽限制的；
• 因此它们会涉及溢出、符号位、底层表示等额外问题。

所以，把 Nat 理解成“和真实语言整数很像的理论近似”是可以的；但不要把二者完全等同。

6.2.4 与真实语言的对照

如果一定要做编程语言类比，更稳妥的说法是：

• Unit 在直觉上接近某些语言里的“无有趣返回值”；
• 但它不应简单等同于 null；
• 某些语言里的 void、某些函数式语言里的 unit，通常更接近这个概念。

6.3 积类型：把两个值放在一起

基础类型解决了“原子值”的分类问题，但程序里经常还需要把多个值组合在一起。例如：

• 一个人的名字和年龄；
• 一个函数返回两个结果；
• 一个节点保存一个值和一个子结构。

这就引出积类型（product type）。

6.3.1 直觉

积类型 $T_1\times T_2$ 表示：

一个值同时包含一个 $T_1$ 类型的部分和一个 $T_2$ 类型的部分。

最简单的例子就是二元组：

$$(t_1,t_2)$$

如果：

• $t_1$ 的类型是 $T_1$
• $t_2$ 的类型是 $T_2$

那么整个二元组的类型就是：

$$T_1\times T_2$$

6.3.2 语法与规则

语法可以扩展为：

$$\begin{array}{rl}T& ::=\dots \mid T_1\times T_2\\ t& ::=\dots \mid (t_1,t_2)\mid t.1\mid t.2\end{array}$$

对应的类型规则：

$$\frac{\Gamma ⊢t_1:T_1\Gamma ⊢t_2:T_2}{\Gamma ⊢(t_1,t_2):T_1\times T_2}\text{(T-Pair)}$$

$$\frac{\Gamma ⊢t:T_1\times T_2}{\Gamma ⊢t.1:T_1}\text{(T-Proj1)}$$

$$\frac{\Gamma ⊢t:T_1\times T_2}{\Gamma ⊢t.2:T_2}\text{(T-Proj2)}$$

这三条规则的意思非常直观：

• 构造二元组时，要分别检查两个分量；
• 取第一分量时，要求原项确实是一个积类型；
• 取第二分量时也是一样。

6.3.3 例子

若：

• $\Gamma ⊢\text{true}:\text{Bool}$
• $\Gamma ⊢0:\text{Nat}$

那么：

$$\Gamma ⊢(\text{true},0):\text{Bool}\times \text{Nat}$$

进一步：

$$\Gamma ⊢(\text{true},0).1:\text{Bool}$$

$$\Gamma ⊢(\text{true},0).2:\text{Nat}$$

6.3.4 积类型与逻辑

在 Curry–Howard 对应下，积类型通常对应逻辑中的合取：

$$A\times B\text{对应}A\wedge B$$

这非常自然：

• 一个 $A\times B$ 类型的值，同时提供一个 $A$ 和一个 $B$；
• 一个命题 $A\wedge B$ 的证明，也意味着你同时拥有 $A$ 和 $B$ 的证明。

6.4 和类型：二选一的值

有些数据不是“同时拥有两部分”，而是“要么是这一种，要么是那一种”。

例如：

• 一个计算结果要么成功，要么失败；
• 一个表达式要么是整数字面量，要么是布尔字面量；
• 一个树节点要么是空，要么是非空结构。

这就引出和类型（sum type）。

6.4.1 直觉

和类型 $T_1+T_2$ 表示：

一个值要么来自左边的 $T_1$，要么来自右边的 $T_2$。

但仅仅说“要么是左边、要么是右边”还不够，因为运行时还必须能区分到底是哪一边。因此和类型的值通常带有一个标记。

常见写法是：

• inl(t)：表示这是左侧分支
• inr(t)：表示这是右侧分支

不过这里要补一个形式化层面的说明。
如果我们采用带显式类型注解的 Church 风格（Church-style）项，那么仅写 inl(t) / inr(t) 往往还不够，因为：

• inl(t) 只告诉你“这是左侧注入”；
• 但没有直接告诉你右侧到底是哪种类型；
• 因而同一个 inl(t) 可能同时属于很多不同的和类型。

所以在更严格、语法制导（syntax-directed）的写法里，常会把它写成类似：

• inl(t) as T1 + T2
• inr(t) as T1 + T2

本章后面的规则先沿用较简洁的 inl(t) / inr(t) 记法，强调其核心直觉；但你应当记住：

若想把和类型写成完全语法制导、可直接检查的 Church 风格系统，注入项通常需要把目标和类型也一并标出来。

也可以换一种理解方式：

• 若不显式写出目标和类型，
• 那么这里展示的就是一种更偏声明式的类型规则，
• 它说明“什么情况下该判断成立”，而不一定直接对应最简洁的检查算法。

6.4.2 语法与规则

语法扩展为：

$$\begin{array}{rl}T& ::=\dots \mid T_1+T_2\\ t& ::=\dots \mid \text{inl}(t)\mid \text{inr}(t)\mid \text{case }t\text{ of inl}(x)\Rightarrow t_1\mid \text{inr}(y)\Rightarrow t_2\end{array}$$

若采用更严格的 Church 风格写法，也可以把前两项改写成：

$$\text{inl}(t)\text{as }{T}_1+T_2\text{inr}(t)\text{as }{T}_1+T_2$$

这样注入项本身就携带了足够的目标类型信息。

类型规则：

$$\frac{\Gamma ⊢t:T_1}{\Gamma ⊢\text{inl}(t):T_1+T_2}\text{(T-Inl)}$$

$$\frac{\Gamma ⊢t:T_2}{\Gamma ⊢\text{inr}(t):T_1+T_2}\text{(T-Inr)}$$

$$\frac{\Gamma ⊢t:T_1+T_2\Gamma ,x:T_1⊢t_1:T\Gamma ,y:T_2⊢t_2:T}{\Gamma ⊢\text{case }t\text{ of inl}(x)\Rightarrow t_1\mid \text{inr}(y)\Rightarrow t_2:T}\text{(T-Case)}$$

最值得注意的是 case 规则：

• 被分析的对象必须确实是和类型；
• 左右两个分支都必须能产生同一个结果类型 $T$；
• 整个 case 表达式的类型才是 $T$。

这和前面的 if 很像：
虽然运行时只会走其中一个分支，但类型系统必须在静态上知道不管走哪边，结果类型都一致。

6.4.3 一个例子

若：

$$\Gamma ⊢0:\text{Nat}$$

则：

$$\Gamma ⊢\text{inl}(0):\text{Nat}+\text{Bool}$$

如果再定义：

• 左分支把自然数转换成某个结果类型 $T$
• 右分支把布尔值也转换成同一个结果类型 $T$

那么整个 case 才是良类型的。

6.4.4 和类型与逻辑

在 Curry–Howard 对应下，和类型通常对应逻辑中的析取：

$$A+B\text{对应}A\vee B$$

因为一个 $A+B$ 类型的值，本质上就是：

• 要么给你一个 $A$；
• 要么给你一个 $B$；
• 并且告诉你是哪一种。

6.5 记录类型：带名字的积类型

普通积类型通过位置来访问分量：

• 第一项
• 第二项

但在实际编程中，我们经常更希望通过字段名访问。
这就引出记录类型（record type）。

6.5.1 直觉

一个记录类型看起来像这样：

$$\{name:\text{String},age:\text{Nat}\}$$

它和积类型的区别不是“本质结构变了”，而是：

• 积类型按位置组织分量；
• 记录类型按名字组织分量。

所以记录类型可以理解为：

带标签的积类型。

不过从后续章节的角度看，还需要再补一句更精确的定位：

本教程后文默认把记录看作按字段名组织的结构类型。

这意味着：

• 记录是否“兼容”，主要看字段集合与字段类型；
• 而不是看某个类型名、类名或继承层次。

这条视角会在第 8 章讨论结构子类型（structural subtyping）时真正进入中心位置。

6.5.2 最小语法与规则骨架

为了让记录类型和前面的积类型、和类型在形式化层级上更平衡，这里给出一个最小骨架。

语法可以写成：

$$\begin{array}{rl}T& ::=\dots \mid \{l_1:T_1,\dots ,l_n:T_n\}\\ t& ::=\dots \mid \{l_1=t_1,\dots ,l_n=t_n\}\mid t.l\end{array}$$

其中：

• l_1,\dots,l_n 是字段名；
• t.l 表示从记录 t 中取出字段 l。

最基本的类型规则形状是：

$$\frac{\Gamma ⊢t_1:T_1\cdots \Gamma ⊢t_n:T_n}{\Gamma ⊢\{l_1=t_1,\dots ,l_n=t_n\}:\{l_1:T_1,\dots ,l_n:T_n\}}\text{(T-Rcd)}$$

以及投影规则：

$$\frac{\Gamma ⊢t:\{l_1:T_1,\dots ,l_n:T_n\}}{\Gamma ⊢t.l_i:T_i}\text{(T-ProjRcd)}$$

这些规则表达的直觉很简单：

• 构造记录时，要分别检查每个字段的值；
• 读取字段时，要求原项确实具有对应字段。

这里不再展开更完整的求值规则，因为本节的重点是建立“按字段名组织数据”的类型直觉，并为第 8 章的记录子类型做准备。

6.5.3 作用

记录类型的重要性不止在于“方便组织数据”。
更重要的是，它为后面第八章的子类型打下基础。

因为一旦有了命名字段，我们就可以自然地讨论：

• 一个包含更多字段的记录，
• 是否可以在只要求其中部分字段的地方使用？

这正是宽度子类型化会研究的问题。

也就是说，第八章里最直观的“记录子类型”例子，其实就是建立在这里的记录类型直觉之上。若你之后读到 S <: T、宽度子类型化、深度子类型化时觉得抽象，可以先回到这一节重新看“按字段名组织数据”这件事。

更进一步说，第 8 章默认采用的是：

结构性记录视角。

也就是说，记录的可替换性由字段结构决定，而不是由名字决定。这一点和很多现实语言中的名义类型（nominal typing）并不相同，阅读时要注意区分。

6.5.4 与现实语言的关系

许多语言中的以下构造，都可以在直觉上和记录类型对应：

• 结构体
• 对象中的字段集合
• 命名元组
• 简单的数据记录

不过要小心：
真实语言中的对象系统通常还涉及方法、继承、可变状态、封装等更多因素，因此不能把“对象 = 记录”简单画等号。更稳妥的说法是：

记录类型提供了面向对象类型系统的一部分基础结构。

6.6 递归类型：让类型引用自己（本章采用同构递归视角）

到目前为止，我们可以表示：

• 原子值
• 二元组
• 二选一的值
• 命名字段的数据

但还不能自然表示列表、树、链表这类自相似结构。
例如，一个整数列表显然应该满足这样的递归描述：

• 要么是空；
• 要么是一个整数，加上一个“更短的整数列表”。

这就需要递归类型（recursive type）。

本节先把立场说清楚：

本章采用的是同构递归（iso-recursive）视角，而不是等价递归（equi-recursive）视角。

也就是说，在本章里：

• μX.T
• 和它展开一层后的 [μX.T/X]T

不会被直接当作“字面上同一个类型”；
它们之间要通过显式的 fold / unfold 来往返。

这条约定很重要，因为后面第 9 章讲类型推断时，还会出现“无限类型（infinite type）为什么被 occur check 拒绝”的问题。那时你需要区分：

• 显式引入的递归类型 μX.T；
• 推断过程中无约束地产生的无限展开类型。

这两者相关，但不是同一回事。

6.6.1 语法直觉

递归类型通常写作：

$$\mu X.T$$

意思是：

• 引入一个类型变量 $X$；
• 允许它在 $T$ 中出现；
• 整个式子表示“把这个自引用封起来”的递归类型。

这里的 $X$ 是类型层面的绑定变量，不要把它和第七章的多态量化混淆。
在这一章里，它只是为了表达递归结构，而不是为了表达“任意类型”。

也正因为本章采用的是同构递归（iso-recursive）视角，所以后面会显式引入 fold 和 unfold；如果采用的是等价递归（equi-recursive）视角，则很多教材会把“展开一层”和“折叠回去”的关系直接并入类型相等。

6.6.2 列表的例子

一个元素类型为 $T$ 的列表，可以写成：

$$\mu L.\text{Unit}+(T\times L)$$

它的意思是：

• 列表要么是空列表，对应 Unit；
• 要么是一个头元素 $T$ 和一个尾列表 $L$ 的二元组。

这里要注意一个细节：
式子里的 $T$ 是“元素类型参数”的占位记号，不是说我们已经进入了第七章那种显式多态系统。更准确地说，这里是在描述：

对于任意一个固定的元素类型 $T$，都可以写出一个相应的列表类型模式。

如果你想把它写得更明确，也可以说：

• 先固定某个元素类型 Elt
• 再定义列表类型为
  $\mu L.\text{Unit}+(\text{Elt}\times L)$

这样更不容易和多态量化混淆。

6.6.3 树的例子

类似地，一个带整数标签的二叉树可以写成：

$$\mu T.\text{Unit}+(\text{Nat}\times T\times T)$$

它表示：

• 要么是空树；
• 要么是一个节点，节点里有一个 Nat 值和两个子树。

6.6.4 折叠与展开

在同构递归的形式化处理中，通常需要两种操作：

• fold
• unfold

其类型规则可写为：

$$\frac{\Gamma ⊢t:[\mu X.T/X]T}{\Gamma ⊢\text{fold}(t):\mu X.T}\text{(T-Fold)}$$

$$\frac{\Gamma ⊢t:\mu X.T}{\Gamma ⊢\text{unfold}(t):[\mu X.T/X]T}\text{(T-Unfold)}$$

直觉上：

• unfold 是把递归类型“打开一层”；
• fold 是把展开后的结构“重新包回去”。

之所以需要这两个操作，是因为在同构递归视角下，类型系统需要精确地区分：

• “递归类型本身”
• 和“它展开一层之后的样子”

如果采用的是等价递归视角，很多教材会把这种“展开一层”和“折叠回去”的关系内化到类型相等里；
而本章没有这样做，正是因为我们选择了更适合入门说明规则结构的 fold / unfold 写法。

这里顺便提前埋一个和第 9 章有关的伏笔：

显式递归类型是语言设计中主动加入的构造；而 HM 推断里的 occur check 所阻止的，是系统在合一过程中无约束地产生无限类型。

因此：

• “允许 μX.T”
  不等于
• “允许把任意类型变量都自动解成无限展开结构”。

这两者要到第 9 章放在一起看，边界才会完全清楚。

6.6.5 递归类型为什么重要？

因为很多最常见的数据结构都依赖递归定义：

• 列表
• 树
• 语法树
• 链表
• 某些对象结构

没有递归类型，语言虽然能表示很多局部数据，但很难自然表达这些层层嵌套的无限族结构。

6.7 可选类型与错误结果：和类型的常见实例

为了帮助你把和类型和真实语言联系起来，这里单独强调两个常见模式。

6.7.1 可选类型

“一个值要么存在，要么不存在”可以自然写成：

$$T+\text{Unit}$$

或者也可以写成：

$$\text{Unit}+T$$

这两种写法本质上都可以表达“可选值”，区别只在于你约定：

• 左边代表空，右边代表有值；
• 还是左边代表有值，右边代表空。

因此，在把某门具体语言的 optional、nullable、maybe 等机制和和类型对应时，最稳妥的说法是：

它们通常可以看作某种和类型编码的直觉对应。

但不要把“左注入一定是空”或“右注入一定是空”当成普遍规则——那只是具体约定。

6.7.2 错误联合与结果类型

“一个计算要么成功返回结果，要么返回错误”也很适合用和类型表达，例如：

$$\text{Result}(E,T)\cong E+T$$

或者反过来：

$$T+E$$

同样，哪一边表示成功、哪一边表示错误，取决于你的具体约定。

这种模式在很多语言里都非常常见，因此和类型不仅是一个理论构造，也是非常实用的程序设计工具。

6.8 可变引用：从纯计算走向状态

到目前为止，本章讨论的构造大多仍然适合纯函数式语言：
值一旦构造出来，就不会被“原地修改”。

但很多实际语言还支持可变存储。
这就引出引用类型（reference type）：

$$\text{Ref}(T)$$

6.8.1 直觉

如果一个项的类型是 $\text{Ref}(T)$，可以把它理解成：

一个指向存储单元的引用，而这个存储单元里应该放一个 $T$ 类型的值。

于是会有三种典型操作：

• 创建引用：ref(t)
• 读取内容：!t
• 写入内容：t_1 := t_2

6.8.2 类型规则

$$\frac{\Gamma ⊢t:T}{\Gamma ⊢\text{ref}(t):\text{Ref}(T)}\text{(T-Ref)}$$

$$\frac{\Gamma ⊢t:\text{Ref}(T)}{\Gamma ⊢!t:T}\text{(T-Deref)}$$

$$\frac{\Gamma ⊢t_1:\text{Ref}(T)\Gamma ⊢t_2:T}{\Gamma ⊢t_1:=t_2:\text{Unit}}\text{(T-Assign)}$$

这些规则表达的都是最自然的直觉：

• 只有当你确实有一个 $T$ 类型的值时，才能创建 Ref(T)；
• 只有当你确实有一个 Ref(T) 时，才能解引用得到 T；
• 只有当引用和写入值的类型匹配时，写入才合法。

6.8.3 为什么引用让系统更复杂？

一旦引入可变引用，程序的计算就不再只是“项自身如何归约”，而变成了：

• 项怎样变化；
• 存储（store）怎样变化。

这意味着第五章里的类型安全证明也要相应升级。
尤其是保持性，不再只需要跟踪项的类型，还要跟踪堆中位置存放的内容类型。

这通常需要额外引入存储类型（store typing）之类的辅助概念。

所以从理论角度说：

可变状态是从纯 Lambda 风格语言走向现实编程语言的重要分水岭。

这里也提前为第 8 章埋一个关键伏笔：

一旦再把子类型加入系统，Ref(T) 的变化方向就会立刻变得微妙。

原因是：

• 读取操作看起来希望它协变；
• 写入操作看起来又希望它逆变；

而这两种要求会彼此冲突。第 8 章讨论“不变性（invariance）”时，会回到这一点。

6.9 与真实语言的对照：应该怎样理解？

这一章里的很多构造在现实语言中都有明显影子，但类比时必须保持克制。

6.9.1 可以安全使用的直觉类比

• 积类型接近二元组、元组、结构体中的“同时包含多个部分”
• 和类型接近枚举、变体、结果类型、可选类型
• 记录类型接近按字段名组织的数据
• 递归类型接近列表、树、链表等自引用数据结构
• 引用类型接近“指向可变存储位置”的引用或地址

6.9.2 不应说得太满的地方

• Unit 不应简单等同于 null
• Nat 不应简单等同于机器整数
• 某门语言的对象系统不应直接等同于记录类型
• 某门语言的 optional / result 机制也不应被说成“就是和类型本身”，更准确的说法是“可用和类型直觉理解”

理论构造和真实语言之间通常是：

相似、相关、可类比，但不严格一一对应。

保持这种边界感，会让后面的多态、子类型和引用讨论更清楚。

6.10 本章小结

这一章在 STLC 的基础上，逐步加入了更丰富的一阶类型构造：

1. 基础类型让我们能够表示布尔值、自然数和单位值。
2. 积类型表示“同时拥有两部分”的值。
3. 和类型表示“二选一”的值，并要求通过分支分析来使用。
4. 记录类型是带字段名的积类型，并为后续的结构子类型讨论打下基础。
5. 递归类型让类型可以表达列表、树等自相似结构；本章明确采用的是同构递归（iso-recursive）视角。
6. 可变引用把语言从纯计算推进到带状态的计算模型，也为后面“为什么引用通常不变”埋下伏笔。

如果把这一章压缩成一句话，那就是：

一阶类型系统的核心任务，是让类型系统能够描述常见的数据形态，而不仅仅是函数。

而从全书主线看，本章向后输出了三条特别重要的线索：

• 第 7 章会继续讨论：如何对类型本身做抽象；
• 第 8 章会回到本章的记录类型与引用类型，讨论结构子类型与变化方向；
• 第 9 章则会从另一个角度回看本章的递归类型，帮助你区分“显式递归类型”和“推断中被 occur check 拒绝的无限类型”。

下一章开始，我们会进一步扩展类型系统的能力，不再只给“具体类型”分类，而是开始讨论：

如何对类型本身做抽象。

回看导航

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

1. 回看第 5 章：重新确认 Γ ⊢ t : T、类型规则与类型安全的基本骨架；
2. 回看附录A：重点查看“基础类型”“积类型”“和类型”“记录类型”“递归类型”“可变引用”“存储类型”等条目；
3. 回看附录B：重点确认 T_1 × T_2、T_1 + T_2、μX.T、Ref(T)、fold、unfold 等记号；
4. 若你准备继续读第 8 章，建议先把本章的“记录类型”和“引用类型”再看一遍，因为它们会直接成为子类型讨论的背景；
5. 若你之后读到第 9 章时对“无限类型为什么被拒绝”感到疑惑，也可以回到本章的递归类型部分，重新确认“显式递归类型”和“推断中自动生成的无限类型”不是同一回事。

本章练习

1. 解释为什么 if t1 then t2 else t3 的两个分支必须有相同类型。
2. 写出一个 Bool × Nat 类型值的例子，并说明如何分别取出它的两个分量。
3. 用自然语言解释类型 $\text{Nat}+\text{Bool}$ 中的值可能长什么样。
4. 说明为什么列表类型可以写成“空列表或头元素加尾列表”的递归形式。
5. 为什么引入 Ref(T) 之后，类型安全证明需要额外跟踪存储的类型信息？