第九章类型推断

前几章中，我们主要讨论的是 Church 风格（Church-style）的类型系统：项里直接写出类型注解，例如 $l amb d a x : T . t$ 。这种做法的优点是规则清楚、类型检查直接，但也有一个明显缺点：

程序员需要手写大量类型注解。

现实中的许多语言并不要求你把所有类型都写出来。相反，编译器会根据程序结构自动推导出类型。这就是本章要讨论的主题：

类型推断（type inference）

阅读提示

本章会频繁使用“Curry 风格（Curry-style）”“约束生成（constraint generation）”“合一（unification）”“类型方案（type scheme）”“泛化（generalization）”“实例化（instantiation）”等术语。若你一时忘了这些词的定义，可随时回查：

附录A《术语表》中的 A.3 和 A.7 相关条目；

附录B《符号速查表》中的“类型推断与合一相关记号”。

同时，也建议把本章和第 7 章一起看：第 7 章讨论的是表达力更强的显式多态系统 System F，而本章讨论的是更适合自动推断的 HM 路线。

本章要回答的问题是：

什么是“推断类型”？
为什么可以把推断问题转化为“生成约束 + 求解约束”？
什么是合一（unification）？
为什么 let 绑定可以多态，而普通函数参数通常不行？

为了聚焦核心思想，本章主要采用 Hindley–Milner（HM）风格 的类型推断视角。

在进入正文之前，先固定一个非常重要的边界：

本章讨论的不是“如何自动推断第 7 章完整 System F 的显式二阶多态”，而是 HM 风格的 let 多态推断。

这两条路线都和“多态”有关，但层级不同：

第 7 章的 ∀X.T、ΛX.t、t[T] 是对象语言中的显式构造；
本章的 ∀α.T 主要出现在环境中的类型方案（type scheme）里，用来支持 let 多态；
因此，HM 可以看作一种表达力更受限、但更适合自动推断的多态路线，而不是“System F 的自动推断版”。

为了减少后文混淆，你可以先把本章中的对象分成三层来看：

项层
- λx.t
- t1 t2
- let x = t1 in t2
类型层
- α, β, γ
- Bool
- T1 -> T2
环境层
- Γ
- 其中变量可能绑定到普通类型，也可能绑定到类型方案

带着这三层区分去读后面的“约束生成、合一、泛化、实例化”，会更不容易把第 7 章的显式多态和本章的 HM 推断混在一起。

9.1 从类型检查到类型推断

第五章里我们做的是类型检查：

项中已经带有类型注解；
我们要验证这些注解是否一致；
判断形式通常是 $Γ ⊢ t : T$ 。

例如，对项：

$λ x : Bool . x$

我们不是“猜”它的类型，而是检查它是否能被规则推出为：

$Bool \to Bool$

而类型推断则不同。它面对的是没有显式类型注解的项。例如：

$λ x . x$

这里的问题不再是“给定注解是否正确”，而是：

这个项最一般的类型是什么？

直觉上你已经知道答案：它应该是“从某个类型到同一类型的函数”。但要把这个直觉变成算法，我们需要一种系统方法。

9.2 Curry 风格：项不写类型，类型由系统赋予

在类型推断的语境下，我们通常使用 Curry 风格（Curry-style）的项，也就是说，项的语法里不直接包含类型注解。

例如：

$t ::= x mi d l amb d a x . t mi d t t mi d t e x t l e t x = t_{1} t e x t in t_{2}$

与 Church 风格相比：

Church 风格： $l amb d a x : T . t$
Curry 风格： $l amb d a x . t$

差别不只是“少写了一个注解”。更深层地说：

Church 风格里，类型检查主要是在验证；
Curry 风格里，类型系统需要恢复这些省略掉的信息。

这就是类型推断的本质。

这里也顺手和第 7 章再做一次区分：

第 7 章里，显式多态项会真的写出 ΛX.t 和 t[T]；
本章里，项语法并不包含这些显式类型层构造；
因而本章的多态能力主要来自 let 绑定的泛化与实例化，而不是对象语言中显式写出的类型抽象与类型应用。

9.3 类型推断想求什么？

给定一个无注解项 $t$ ，类型推断希望找到一个类型 $T$ ，使得：

$Γ ⊢ t : T$

在简单例子里，这看起来像是在“直接猜类型”。但在实际算法中，我们不会一开始就猜中，而是：

先为未知类型位置放入类型变量
再从程序结构中生成约束
最后求解这些约束

例如，对项：

$λ f . λ x . f x$

我们可以先假设：

$f : α$
$x : β$
应用结果 $f x : γ$

接着根据函数应用的结构知道：

如果 $f x$ 成立，那么 $f$ 必须是一个函数
它的参数类型必须和 $x$ 的类型一致
它的返回类型就是整个应用的结果类型

于是得到约束：

$α = β \to γ$

最后把这个约束解出来，就得到整个项的类型。

这就是 HM 推断的基本工作流。

9.4 约束生成：先把未知处都记下来

类型推断的第一步，不是立刻求答案，而是先把“必须满足什么条件”收集出来。

9.4.1 类型变量

我们用希腊字母表示未知类型：

$α, β, γ, \dots$

它们不是具体类型，而是“待求解的占位符”。

例如：

一个还不知道参数类型的函数参数可以记作 $α$
一个还不知道结果类型的表达式可以记作 $β$

9.4.2 约束的来源

约束并不是凭空产生的，它来自类型规则的逆向阅读。

例如，应用规则在第五章写作：

$\frac{Γ ⊢ t _{1} : T _{1} \to T _{2} Γ ⊢ t _{2} : T _{1}}{Γ ⊢ t _{1} t _{2} : T _{2}}$

反过来读它就是：

如果我想给 t1 t2 找类型，
那就必须让 t1 的类型是某个函数类型，
并且它的参数类型与 t2 的类型匹配。

于是应用结构天然会产生“两个类型必须相等”之类的约束。

9.5 一个完整例子：推断 $l amb d a f . l amb d a x . f x$

现在我们完整走一遍最经典的例子：

$l amb d a f . l amb d a x . f x$

第一步：给未知部分分配类型变量

设：

$f : a lp ha$
$x : b e t a$
$f x : g amma$

那么整个项的外形是：

$l amb d a x . f x$ 的类型应为 $b e t a t o g amma$
$l amb d a f . l amb d a x . f x$ 的类型应为 $a lp ha t o b e t a t o g amma$

第二步：由应用结构生成约束

子项 $f x$ 是一个函数应用。

根据应用规则：

$f$ 必须是一个函数；
其参数类型必须是 $b e t a$ ；
其返回类型必须是 $g amma$ 。

因此得到约束：

$a lp ha = b e t a t o g amma$

第三步：求解约束

将约束解出后，把它代回整体类型：

$a lp ha t o b e t a t o g amma$

代入 $a lp ha = b e t a t o g amma$ ，得到：

$(b e t a t o g amma) t o b e t a t o g amma$

第四步：得到最一般单态类型

这里要特别注意层级。

对这个裸 Lambda 项来说，我们首先得到的是它的最一般单态类型：

$(b e t a t o g amma) t o b e t a t o g amma$

之所以这里先说“单态类型”，是因为在标准 HM 里：

对项结构本身做推断时，先得到的是带类型变量的普通类型；
只有当某个定义进入 let 绑定环境时，才会进一步触发泛化（generalization），把它提升成类型方案。

因此，更精确地说：

这个项的最一般单态类型是 $(b e t a t o g amma) t o b e t a t o g amma$
若把它放到顶层、或放到可泛化的位置来记录，也可以把对应的最一般类型方案（principal type scheme）写成 $f or a ll b e t a, g amma . (b e t a t o g amma) t o b e t a t o g amma$

这正是我们熟悉的“函数应用器”类型。

9.6 合一：怎样求解类型等式？

约束生成之后，我们得到的是一组类型等式。接下来必须解决的问题是：

怎样求出一组替换，使这些等式同时成立？

这就是合一（unification）。

9.6.1 替换

一个替换 $σ$ 把类型变量映射为类型，例如：

$σ = [α \mapsto Bool, β \mapsto Nat \to Nat]$

把它作用到类型上时，就把对应变量替换掉。

例如：

$σ (α \to β) = Bool \to (Nat \to Nat)$

本章里我们统一约定：

$s i g ma$ 保留给替换使用；
类型方案不用 $s i g ma$ 记，而改用 Sch（scheme）或文字说明。

这样可以避免“同一个符号既表示替换、又表示类型方案”的混淆。

9.6.2 合一问题

如果我们有一组约束，例如：

$α = β \to γ$

那么一个合一器就是某个替换 $σ$ ，使得：

$σ (α) = σ (β \to γ)$

成立。

例如：

$[α \mapsto β \to γ]$

就是这个单个约束的一个合一器。

但更常见的是有多条约束要一起解，例如：

$α = β \to γ, β = Bool$

这时就需要一个替换同时满足两条约束。

9.7 合一算法的核心规则

合一算法的目标是：输入一组类型等式，输出一个最一般合一器（most general unifier, MGU），如果不存在就失败。

最核心的几类情形如下。

9.7.1 相同类型

若约束为：

$T = T$

那么它已经自动成立，不需要额外替换。

9.7.2 类型变量与类型相等

若约束为：

$α = T$

只要 $α$ 不出现在 $T$ 中，就可以产生替换：

$[α \mapsto T]$

这是合一算法中最基本的一步。

对称地，若有：

$T = α$

也同样处理。

9.7.3 函数类型相等

若约束为：

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

那么这不是“一步就能直接解完”的，而是要拆成两个更小的约束：

$T_{1} = U_{1} T_{2} = U_{2}$

也就是说，两个函数类型相等，当且仅当：

参数类型相等
返回类型相等

9.7.4 其他构造子不匹配则失败

例如：

$Bool = Nat$

显然无解。

同样，如果两个类型的最外层构造子不同，也无法合一。

9.8 为什么要做 occur check？

在处理约束

$a lp ha = T$

时，有一个非常重要的附加检查：

$a lp ha$ 不能出现在 $T$ 中。

这叫 occur check。

9.8.1 一个危险例子

考虑约束：

$a lp ha = a lp ha t o b e t a$

如果你试图直接替换：

$[a lp ha ma p s t o a lp ha t o b e t a]$

就会得到无限展开：

$a lp ha = a lp ha t o b e t a = (a lp ha t o b e t a) t o b e t a = ((a lp ha t o b e t a) t o b e t a) t o b e t a = c d o t s$

这意味着我们实际上在试图构造一个无限类型（infinite type）。

标准的 HM 系统不允许这种无限类型，因此这里必须判定为合一失败。

所以 occur check 的意义就是：

防止类型推断偷偷构造出无限递归类型。

这里要特别和第 6 章的递归类型（recursive type）区分开来。二者不是同一回事：

第 6 章里的 μX.T 是显式引入的递归类型构造；
而这里 occur check 阻止的是：在标准 HM 合一过程中，把一个普通类型变量隐式解成无限展开结构。

也就是说：

“允许显式递归类型”
和
“允许 HM 在没有额外构造的情况下自动推断出无限类型”

不是同一个问题。

这也是为什么第 6 章可以合法讨论 μX.T，而本章仍然必须拒绝 \\alpha = \\alpha \\to \\beta 这样的约束。

9.9 合一算法中的“替换传播”与“替换组合”

这是本章最容易被写错、也最值得澄清的地方。

很多初学者会误以为，若要合一：

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

只需分别求解：

$T_{1} = U_{1}$
$T_{2} = U_{2}$

然后把两个结果“并集”起来。

但这并不准确。真正正确的做法是：

先求出第一部分的合一器 $σ_{1}$
用 $σ_{1}$ 去改写剩余约束
再求剩余约束的合一器 $σ_{2}$
最终结果是替换的组合 $σ_{2} \circ σ_{1}$

9.9.1 为什么不能直接做“并集”？

因为前一步求出的替换会影响后面的约束。

例如，若有：

$α \to α = Bool \to β$

正确过程是：

先解参数部分： $α = Bool$ ，得到 $σ_{1} = [α \mapsto Bool]$
再把它作用到返回部分约束 $α = β$ 上，得到： $Bool = β$
继续求解，得到： $σ_{2} = [β \mapsto Bool]$
最终替换是： $σ_{2} \circ σ_{1}$

如果你只是把两个结果“并起来”而不传播前一步替换，就会漏掉这种依赖关系。

9.9.2 更准确的函数类型合一写法

因此，函数类型合一更准确地写成：

先令 $σ_{1} = unify (T_{1} = U_{1})$
再令 $σ_{2} = unify (σ_{1} (T_{2}) = σ_{1} (U_{2}))$
最终结果为： $σ_{2} \circ σ_{1}$

这就是标准算法里的“先解、再传播、再组合”。

9.10 一个失败例子：为什么 $λ x . x x$ 无法推断？

这是 HM 系统里最经典的失败案例之一。

考虑项：

$λ x . x x$

第一步：分配类型变量

设：

$x : α$
$x x : β$

第二步：生成约束

由于 x x 是函数应用：

函数位置 x 必须是某个函数类型
参数位置 x 必须匹配其参数类型

于是得到：

$α = α \to β$

第三步：尝试合一

这里立刻触发 occur check：

左边是 $α$
右边是 $α \to β$
$α$ 出现在右边

因此无解。

这说明：

在标准 HM 系统中， $λ x . x x$ 不可类型化。

这个例子非常重要，因为它让你看到：

不是所有无注解 Lambda 项都能被 HM 推断；
失败并不是算法“太弱”，而是该系统本身就不允许这种无限类型。

9.11 let 多态：为什么 `let` 可以多态复用？

到目前为止，我们得到的类型都还是“单次使用视角”下的。
但真实语言里，一个函数经常希望在多个不同类型上复用。

例如：

let id = fun x -> x in
  (id true, id 1)

这里 id 被用了两次：

一次作用于 Bool
一次作用于 Nat

如果 id 只能有一个固定单态类型，这就不成立了。

于是 HM 系统引入了一个非常关键的机制：

let 绑定可以在绑定点进行泛化（generalization），在使用点进行实例化（instantiation）。

9.12 类型方案：不只是一个类型，而是一族类型

为了表达“同一个名字可以在不同地方按不同实例使用”，我们引入类型方案（type scheme）。

为了避免与前面“替换”使用的 $s i g ma$ 记号冲突，这里把类型方案记作：

$S c h ::= T mi d f or a ll a lp h a_{1} d o t s a lp h a_{n} . T$

例如：

$f or a ll a lp ha . a lp ha t o a lp ha$

表示的不是某一个具体类型，而是一族类型：

Bool -> Bool
Nat -> Nat
String -> String
…

这正是恒等函数 id 最一般的多态类型。

如果你把这一节和第 7 章对照起来看，会发现一个非常重要的区别：

第 7 章里的 ∀X.T 是对象语言中的显式多态类型构造；
本章里的类型方案主要服务于 HM 推断中的环境记录、泛化与实例化；
第 7 章还会配套出现显式项构造 ΛX.t 与 t[T]；
而本章的项语法里并没有这些显式类型层构造。

因此，虽然两边都写 ∀，但它们不是同一个层次上的东西。更准确地说：

第 7 章讨论的是显式写进对象语言的多态；本章讨论的是 HM 环境中的 let 多态。

这也是为什么本章不应被理解成“自动推断完整 System F”，而应理解成：

在表达力更受限的前提下，用类型方案、泛化和实例化来获得可判定、可实现的多态推断。

9.13 泛化（generalization）

当我们看到：

let x = t1 in t2

类型推断的基本思路是：

先推断 t1 的类型为 $T$
找出 $T$ 中那些不被当前环境固定住的类型变量
对这些变量做全称量化，得到类型方案
再把这个类型方案绑定给 x，继续推断 t2

形式上，常写成：

$Gen (Γ, T) = \forall \overline{α} . T$

其中 $\overline{α}$ 是满足以下条件的类型变量集合：

出现在 $T$ 中
但不自由出现在环境 $Γ$ 中

直觉上，这表示：

若某个类型变量不受当前环境限制，
那它就是真正“任意的”，
因此可以被泛化成多态变量。

9.14 实例化（instantiation）

一旦某个名字在环境中绑定的是类型方案，例如：

$i d : \forall α . α \to α$

那么每次使用它时，都可以把其中量化的类型变量换成新的实例。

例如：

第一次用 id 时实例化成： $Bool \to Bool$
第二次用 id 时实例化成： $Nat \to Nat$

这个过程叫实例化。

其本质是：

每次取出一个多态绑定时，都为其中量化变量生成一份新的、彼此独立的类型变量副本。

这一步非常重要。
如果不生成“新鲜副本”，不同使用位置就会互相干扰，错误地把本应独立的实例绑在一起。

这也正是 HM 与第 7 章 System F 的一个重要阅读分界：

第 7 章强调“多态如何被显式写进项和类型里”；
本章强调“编译器如何在较受限但可判定的框架里自动恢复这种多态信息”。

因此，本章讨论 let 多态时，最好始终带着这条比较线索来看。

9.15 一个 let 多态的完整直觉例子

考虑：

let id = fun x -> x in
  (id true, id 0)

第一步：推断右侧定义

对 fun x -> x，我们已知可推断出：

$α \to α$

第二步：泛化

若当前环境没有约束这个 $α$ ，那么可泛化为：

$\forall α . α \to α$

于是环境里记录：

$i d : \forall α . α \to α$

第三步：在使用点分别实例化

第一次使用 id true：

实例化为 $Bool \to Bool$

第二次使用 id 0：

实例化为 $Nat \to Nat$

由于这两次实例化彼此独立，因此整个表达式良类型。

这就是 HM 系统里 let 多态的核心。

9.16 为什么函数参数通常不能这样多态？

考虑：

fun id -> (id true, id 0)

直觉上，它和前面的 let id = ... in ... 很像，但在标准 HM 系统中，这个表达式通常不合法。

原因在于：

fun id -> ... 中的 id 是一个普通参数；
参数进入环境时只得到一个单态类型变量，例如 $α$ ；
接着由 id true 得知： $α = Bool \to β$
又由 id 0 得知： $α = Nat \to γ$

于是必须同时满足：

$Bool \to β = Nat \to γ$

显然无解。

这说明：

在标准 HM 中，普通函数参数是单态的；只有 let 绑定会触发泛化。

这也是为什么 HM 常被概括为：

let-polymorphism，而不是 full polymorphism

9.17 算法 W 的核心思想（直觉版）

经典的 HM 推断算法常被称为 算法 W（Algorithm W）。
这一节只给出它的核心骨架与工作直觉，不展开完整实现细节、正确性证明和所有工程优化。

对于一个项，算法 W 返回：

一个替换 $s i g ma$
一个类型 $T$

记作：

$W (G amma, t) = (s i g ma, T)$

意思是：

在环境 $G amma$ 下，项 $t$ 经推断得到类型 $T$ ，但这个结果成立的前提是要应用替换 $s i g ma$ 。

它对不同语法构造大致这样处理：

变量

从环境中取出其类型方案
实例化为一个新类型

抽象

给参数分配一个新类型变量
在扩展环境下递归推断函数体
组合结果得到函数类型

应用

分别推断函数和参数
生成“函数类型必须匹配”的新约束
调用合一
组合替换

let

先推断右侧定义
对结果做泛化
将泛化后的类型方案加入环境
再推断主体

如果你理解了“替换传播”和“let 的泛化 / 实例化”，那么算法 W 的主干就已经掌握了。

这里也再强调一次本章边界：

算法 W 服务的是 HM 风格的 let 多态推断；
它并不是“对第 7 章完整显式 System F 做自动推断”的通用算法；
这正体现了 HM 路线的核心取舍：牺牲一部分显式多态表达力，换取更好的自动推断性。

9.18 本章与现实语言的关系

HM 类型推断之所以重要，是因为它抓住了一个很强的工程平衡点：

类型注解可以大量省略；
推断依然可判定；
还能得到很一般的多态类型。

这正是 ML 家族语言成功的重要原因之一。

但也要注意边界：

完整的 System F 类型推断是不可判定的；
很多现代语言只采用 HM 的一部分思想；
实际工业语言常混合使用显式注解、局部推断、子类型、类型类、trait 约束等机制。

因此，更稳妥的说法是：

HM 不是“所有语言推断的统一模型”，但它是理解类型推断最重要的理论起点。

如果你在读到这里时想把主线再串一次，比较推荐的回看顺序是：

回看第 5 章：Γ ⊢ t : T 到底在表达什么；
回看第 7 章：为什么更强的显式多态系统会让自动推断变难；
再回到本章：理解 HM 为什么选择“受限表达力 + 良好可推断性”的平衡点。

9.19 本章小结

这一章的核心内容可以压缩成下面几句话：

类型推断解决的是：在没有显式类型注解时，如何自动恢复类型。
标准方法是：
- 为未知位置分配类型变量；
- 从项结构中生成约束；
- 用合一求解这些约束。
合一算法的关键点包括：
- 类型变量替换；
- 构造子分解；
- occur check；
- 替换的传播与组合。
对函数类型的合一，不能把两个子问题的结果简单做“并集”，而必须：
- 先求第一部分；
- 再把替换传播到第二部分；
- 最后组合替换。
let 多态的本质是：
- 在 let 绑定处做泛化；
- 在使用处做实例化。
标准 HM 中：
- let 绑定可以是多态的；
- 普通函数参数通常是单态的。

如果你读完本章，已经能清楚回答下面三个问题，就说明你真正掌握了主线：

为什么约束来自类型规则的逆向阅读？
为什么合一需要替换传播，而不是简单拼接结果？
为什么 let id = ... in ... 可以多态，而 fun id -> ... 通常不行？

回看导航

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

回看第 5 章：重新确认 Γ ⊢ t : T 到底在表达什么，以及类型规则为何能被“逆向阅读”为约束。
回看第 7 章：重新比较显式多态 System F 与 HM 风格推断的区别，尤其注意“表达力更强”与“更难自动推断”之间的关系。
配合附录A《术语表》：重点回看“约束生成”“合一”“类型方案”“泛化”“实例化”“let 多态”“算法 W”“主类型”“主类型方案”。
配合附录B《符号速查表》：重点确认 \\alpha,\\beta,\\gamma、\\sigma、\\sigma_2 \\circ \\sigma_1、\\text{unify}(\\cdots)、\\text{Gen}(\\Gamma, T) 这些记号。
最后再回做本章练习：如果你已经能独立手工生成约束、执行合一，并解释 let 多态为何成立，就说明这一章已经真正站稳了。

本章练习

推断下列项的最一般类型：
- $λ x . x$
- $λ f . λ x . f x$
- $λ x . λ y . x$
对项 $λ x . x x$ 手工生成约束，并说明为什么合一失败。
对约束组 $α \to α = Bool \to β$ 手工执行合一步骤，写出每次得到的替换以及最终结果。
解释为什么下面的表达式在 HM 中可以通过：
```
let id = fun x -> x in (id true, id 0)
```
解释为什么下面的表达式在标准 HM 中通常不能通过：
```
fun id -> (id true, id 0)
```
用自己的话说明：
- 泛化做了什么？
- 实例化做了什么？
- 为什么二者必须配合出现？

下一章，我们将转向另一个与“资源使用方式”相关的重要方向：子结构类型系统。那时，类型不再只描述“值是什么形状”，还会开始描述“值应该怎样被使用”。

Keyboard shortcuts

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