第五章类型系统核心概念

前两章建立了形式化工具，第 3–4 章建立了计算模型。现在终于可以进入本教程的核心问题：

我们怎样在程序运行之前，排除某些运行时错误？

本章要回答的问题是：

什么叫“一个项有某个类型”？
类型规则到底在检查什么？
为什么这些规则能阻止程序“卡住”？

阅读提示

本章会频繁使用 Γ ⊢ t : T、进展性（progress）、保持性（preservation）、类型安全（type safety）等术语。若你一时记不清它们的定义，可随时回查：

附录A《术语表》中的 A.3“类型系统核心术语”；

附录B《符号速查表》中的“逻辑与判断相关记号”“类型系统相关记号”。

同时，本章直接依赖：

第 3 章中的自由变量、替换（substitution）与避免捕获的替换；

第 4 章中的值（value）、小步语义（small-step semantics）与“卡住”。

这一章的任务，就是把这个问题形式化。我们会在一个最小而经典的语言上完成这件事：简单类型 Lambda 演算（Simply Typed Lambda Calculus，简称 STLC）。

不过这里要先固定一个本章约定：

本章的对象语言不是“只有函数的最纯 STLC 片段”，而是“以 STLC 为核心、加入布尔值与条件表达式的最小扩展语言”。

这样做的原因很简单：

纯函数片段当然足以建立类型判断的基本骨架；
但加入 Bool 与 if 之后，“把布尔值当函数用”这类卡住例子会更直观；
因而更适合在入门阶段把“类型系统到底在防什么”讲清楚。

和前几章一样，本章的重点不是一下子记住所有规则，而是先抓住主线：

什么叫“一个项有某个类型”？
类型规则到底在检查什么？
为什么这些规则能阻止程序“卡住”？

5.1 从“卡住”到“有类型”

第四章里我们已经见过“卡住状态”（stuck term / stuck state）这个概念。直观地说：

一个项如果既不是一个正常结果，又无法继续按照求值规则前进，那么它就卡住了。

例如，在一个同时含有布尔值和函数的语言里，下面这样的项就是典型的卡住项：

$true (λ x . x)$

问题不在于它“语法不合法”，而在于它没有合理的计算规则：

true 不是函数；
因此不能把它应用到参数上；
这个项不是值，也不能继续求值。

这正是类型系统想排除的情形。它的基本思路可以概括为：

先给项分类；
分类的名字就叫类型；
然后只允许那些符合规则的组合方式出现。

于是，像“把布尔值当函数用”这种错误，就能在运行前被识别出来。

5.2 什么是类型系统？

Cardelli 的经典定义是：

类型系统（type system）是一种可判定的语法方法，通过对程序短语按其计算值的种类进行分类，来证明程序的某些行为不会发生。

把它放到这一章的语境里，可以读成：

可判定：存在一种检查过程，能够在有限时间内判断程序是否符合类型规则；
语法方法：主要根据程序结构来检查，而不是先运行程序；
分类：把项分成“布尔值”“函数”“积类型值”等不同种类；
某些行为不会发生：类型系统不是万能的，它只保证排除我们关心的那类错误。

因此，Milner 的著名口号：

Well-typed programs cannot go wrong.

更适合被理解为：

在选定的语言和错误模型下，良类型程序不会发生被类型系统禁止的那类错误。

这句话很重要，但也要克制理解。它并不意味着：

良类型程序一定得到你想要的业务结果；
良类型程序一定终止；
良类型程序一定高效。

类型系统保证的是一种受限但有力的可靠性。

5.3 本章使用的对象语言：带布尔值与条件表达式的 STLC 扩展

为了讨论类型系统，我们需要一门足够小、又足够能体现“卡住问题”的语言。

如果只看最纯粹的 STLC 函数片段，很多“明显的类型错误”其实没那么直观；因此本章采用一个带布尔值和条件表达式的 STLC 扩展。这样一来：

我们有函数；
也有基础类型 Bool；
还可以明确展示“把布尔值当函数”之类的错误。

因此，后文若无特别说明：

“本章对象语言”都应理解为“以 STLC 为核心、加入 Bool 与 if 的最小扩展语言”。

5.3.1 类型、项和值

类型定义为：

$T ::= Bool ∣ T_{1} \to T_{2}$

项定义为：

$t ::= x ∣ λ x : T . t ∣ t t ∣ true ∣ false ∣ if t then t else t$

值定义为：

$v ::= λ x : T . t ∣ true ∣ false$

也就是说，在这一章里我们只考虑两类类型：

Bool
函数类型 $T_{1} \to T_{2}$

对应地，项包含：

变量
函数抽象
函数应用
布尔常量
条件表达式

5.3.2 为什么要有类型注解？

注意这里的抽象写成：

$λ x : T . t$

而不是：

$λ x . t$

这意味着我们采用的是 Church 风格（Church-style）：函数参数的类型直接写在项里。这样做的好处是：

类型检查更直接；
规则更容易写成语法制导（syntax-directed）形式；
也更适合作为本教程入门阶段的对象语言。

第九章讲类型推断时，我们会再回头看不显式标注类型的 Curry 风格（Curry-style）。

5.4 类型判断：形式上到底在说什么？

类型系统的核心判断叫做类型判断（type judgment），写作：

$Γ ⊢ t : T$

读作：

在类型环境 $Γ$ 下，项 $t$ 的类型是 $T$ 。

如果你对这个记号的读法还不熟，可以同时回看：

附录A中的“类型判断”“类型环境”条目；
附录B中的 Γ ⊢ t : T 与 ⊢ 记号说明。

这里有三个组成部分：

$Γ$ ：类型环境
$t$ ：项
$T$ ：类型

5.4.1 类型环境

类型环境（type context / typing environment）是“变量到类型”的有限映射，通常写成：

$Γ = x_{1} : T_{1}, x_{2} : T_{2}, \dots, x_{n} : T_{n}$

它的作用很直观：
当你在函数体里遇到一个变量时，必须知道它被假定成什么类型。

例如：

在环境 $x : Bool$ 下，变量 x 的类型就是 Bool
在环境 $f : Bool \to Bool, x : Bool$ 下，项 f x 应该能判断成 Bool

可以把环境理解为一种形式化的“作用域上下文”。

5.4.2 一个直观例子

判断

$x : Bool ⊢ x : Bool$

表示：

假设变量 x 被赋予类型 Bool
那么项 x 的类型就是 Bool

而判断

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

表示：

在空环境下
恒等函数 λx:Bool.x
的类型是 Bool → Bool

这种“环境下的判断”形式，会在后面所有类型规则里反复出现。

5.5 STLC 的类型规则

现在进入本章最核心的部分：类型规则。

5.5.1 变量规则

$Γ ⊢ x : T (Var) 若 Γ (x) = T$

这条规则的意思是：

如果环境里记着 x 的类型是 T
那么就可以判断 x : T

这是一条公理式规则，没有前提。

5.5.2 抽象规则

$\frac{Γ , x : T _{1} ⊢ t : T _{2}}{Γ ⊢ λ x : T _{1} . t : T _{1} \to T _{2}} (Abs)$

这条规则表达了函数的最基本思想：

假设参数 x 的类型是 $T_{1}$
如果在这个假设下，函数体 t 的类型是 $T_{2}$
那么整个函数的类型就是 $T_{1} \to T_{2}$

也就是说，函数类型来自两部分：

参数类型
返回类型

5.5.3 应用规则

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

它的意思是：

若 $t_{1}$ 是一个从 $T_{1}$ 到 $T_{2}$ 的函数；
且 $t_{2}$ 恰好是一个 $T_{1}$ 类型的参数；
那么把 $t_{1}$ 应用于 $t_{2}$ 的结果类型就是 $T_{2}$ 。

这是整章最重要的一条规则之一。
它精确表达了“函数调用必须类型匹配”。

5.5.4 布尔常量规则

$Γ ⊢ true : Bool (True)$

$Γ ⊢ false : Bool (False)$

这两条规则很简单：

true 的类型是 Bool
false 的类型也是 Bool

5.5.5 条件表达式规则

$\frac{Γ ⊢ t _{1} : Bool Γ ⊢ t _{2} : T Γ ⊢ t _{3} : T}{Γ ⊢ if t _{1} then t _{2} else t _{3} : T} (If)$

这条规则说：

条件位置必须是布尔类型；
两个分支必须具有同一个类型；
整个 if 表达式的类型就是那个共同的类型。

最后这一点非常关键。因为程序运行时会走哪一个分支，取决于条件真假；所以如果两个分支类型不同，整个表达式就无法有一个统一的类型。

5.6 如何读类型规则？

对初学者来说，最容易出问题的地方不是规则本身，而是不知道应该从哪里看起。

一个实用方法是：

从下往上看：这条规则允许我推出什么结论？
从上往下看：为了得到这个结论，我需要先满足哪些前提？

例如看应用规则：

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

你可以这样读：

想证明 t1 t2 的类型是 $T_{2}$
我就必须先证明：
- t1 是一个函数，类型为 $T_{1} \to T_{2}$
- t2 是它期望的参数类型 $T_{1}$

这就是“按规则反向构造推导”的基本思路。

5.7 一个完整的推导树示例

我们来证明：

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

这个项的直觉含义是：

接收一个布尔值 x
再接收一个布尔值 y
返回第一个参数 x

5.7.1 证明思路

最外层是一个抽象，所以最后一步一定使用 (Abs)：

若要证明整个项的类型是 Bool → Bool → Bool
就需要在环境 x:Bool 下证明内层函数的类型是 Bool → Bool

内层仍然是抽象，再用一次 (Abs)：

若要证明 $λ y : Bool . x$ 的类型是 Bool → Bool
就需要在环境 x:Bool, y:Bool 下证明 x : Bool

最后这个结论由 (Var) 直接得到。

5.7.2 推导树

$\frac{\frac{x : Bool , y : Bool ⊢ x : Bool (Var)}{x : Bool ⊢ λ y : Bool . x : Bool \to Bool} (Abs)}{⊢ λ x : Bool . λ y : Bool . x : Bool \to Bool \to Bool} (Abs)$

这个例子很重要，因为它展示了：

类型判断不是“拍脑袋决定”；
而是严格由规则一步步推出；
一棵推导树，就是“这个项确实有这个类型”的正式证据。

5.8 为什么有些项无法通过类型检查？

类型系统的力量，恰恰体现在它拒绝某些项。

来看这个项：

$true (λ x : Bool . x)$

如果想用 (App) 规则给它判类型，就必须满足：

函数位置 true 的类型必须是某个函数类型 $T_{1} \to T_{2}$
参数位置 λx:Bool.x 的类型必须是 $T_{1}$

但问题在于：

$true : Bool$

而不是某个函数类型。

所以这个项没有办法构造出合法的类型推导树。也就是说：

它在类型系统里根本不是良类型项。

这就是类型系统排除“把布尔值当函数使用”的方式。它不是等程序运行出错后再抱怨，而是在构造推导树这一步就卡住了。

5.9 从类型规则到类型检查

目前为止，我们写出的都是声明式规则（declarative typing rules）：

它们说明什么样的判断成立；
但还没有明确告诉你，编译器应当如何实现检查。

这里的“声明式规则”和“语法制导”也是后续章节会反复使用的关键词；若你想快速确认定义，可回查附录A中的“类型规则”“语法制导”“类型检查”等条目。

对 STLC 来说，这个实现过程相当直接，因为它的规则是语法制导（syntax-directed）的：

遇到变量，就查环境；
遇到抽象，就扩展环境并递归检查函数体；
遇到应用，就分别检查函数和参数，再判断是否匹配；
遇到 if，就检查条件是不是 Bool，并确认两个分支类型一致。

也就是说，这里要区分两层东西：

声明式规则回答“什么情况下判断成立”；
语法制导检查过程回答“编译器怎样沿语法树把这个判断算出来”。

在本章这个最小系统里，这两层非常接近；但到后面更复杂的系统中，它们未必总是完全重合。

这就是为什么 STLC 的类型检查是可判定的。它不是通过复杂搜索得到的，而是沿着语法树递归进行。

更准确地说：

STLC 的类型判断关系可以被实现为一个总会终止的检查算法。

这和后面第九章的“类型推断”不同。
本章是在已知注解的前提下做类型检查；第九章则会讨论在没有显式注解时，如何自动推断类型。

5.10 类型安全：本章真正要到达的地方

写出类型规则还不够。我们还要回答一个更重要的问题：

为什么这些规则真的能阻止程序卡住？

类型理论里最经典的答案是：类型安全 = 进展性 + 保持性。

5.10.1 进展性（Progress）

进展性（progress）说的是：

一个良类型的封闭项，要么已经是值，要么还可以继续求值。

形式上可写为：

$若 ⊢ t : T ，则 t 是值，或存在 t^{'} 使得 t ⟶ t^{'}$

它排除了什么？
它排除的是“既不是值，又走不动”的情况，也就是卡住状态。

5.10.2 保持性（Preservation）

保持性（preservation）说的是：

如果一个项在求值前有类型 $T$ ，那么它求值一步之后，类型仍然是 $T$ 。

形式上可写为：

$若 Γ ⊢ t : T 且 t ⟶ t^{'} ，则 Γ ⊢ t^{'} : T$

它说明：

求值不会把一个良类型项“算坏”；
计算过程保持类型结构的一致性。

5.10.3 两者合起来意味着什么？

进展性保证：良类型程序不会卡住；
保持性保证：良类型程序在每一步计算后仍然良类型。

合起来就得到：

从一个良类型程序出发，整个计算过程始终不会掉进被类型系统禁止的坏状态。

这才是“良类型程序不会出错”这句话在形式化里的真正内容。

5.11 为什么保持性会依赖替换？

保持性的核心难点，其实来自第四章的 β-归约：

$(λ x : T . t) v ⟶ [x \mapsto v] t$

也就是说，函数应用真正做的事是：

把参数 v
替换进函数体 t
然后继续计算

因此，第五章的类型安全证明并不是凭空开始的，而是直接建立在：

第 3 章的替换与避免捕获的替换；
第 4 章的小步语义与“前进一步”的定义

之上。

因此，要证明保持性，通常需要一个关键引理：替换引理。

替换引理（substitution lemma）

$若 Γ, x : T_{1} ⊢ t : T_{2} 且 Γ ⊢ v : T_{1} ，则 Γ ⊢ [x \mapsto v] t : T_{2}$

它的直觉含义是：

如果 t 在假设 x : T1 时是良类型的，而 v 本身确实是一个 T1 类型的值，那么把 v 替换给 x 之后，整体仍然保持原来的类型。

这正是第三章为什么要严肃定义“避免捕获的替换”的原因：
替换不仅是计算规则的一部分，也是类型安全证明的一部分。

5.12 一个小例子：类型安全如何发挥作用？

看下面这个项：

$(λ x : Bool . x) true$

它显然是良类型的，类型为 Bool。

求值一步：

$(λ x : Bool . x) true ⟶ true$

此时：

原项类型是 Bool
求值后的结果仍然是 Bool

这体现了保持性。

同时，原项也不是卡住的：

它不是值；
但它可以继续归约一步。

这体现了进展性。

反过来看：

$true (λ x : Bool . x)$

这个项没有类型，因此不在“类型安全”定理的适用范围内。类型安全不是说“所有项都不会卡住”，而是说：

所有良类型项都不会卡住。

这个限定一定要记住。

5.13 Church 风格、Curry 风格与本章的定位

前面已经提到，本章采用的是 Church 风格（Church-style）：

项里直接写类型注解；
我们做的是“检查”。

而在 Curry 风格（Curry-style）中：

项本身不携带类型注解；
需要依靠推断或外部规则给项指派类型。

例如：

Church 风格： $λ x : Bool . x$
Curry 风格： $λ x . x$

两者的差别，不只是“写没写注解”，更关系到：

类型检查是否直接；
是否需要类型推断；
能否得到最一般类型。

本章故意选择 Church 风格，不是因为它“更高级”，而是因为：

对入门阶段来说，它最能清楚展示“类型规则如何工作”。

第九章再讨论 Curry 风格和 Hindley–Milner 推断，会更自然。

5.14 Curry–Howard：为什么函数类型像逻辑蕴含？（选读）

这一节不是本章主线，但值得知道它的直觉。

在合适的构造性逻辑系统里，存在一种深刻对应：

类型对应命题；
项对应证明；
函数类型 $A \to B$ 对应逻辑蕴含 $A \Rightarrow B$ 。

为什么？

看抽象规则：

$\frac{Γ , x : T _{1} ⊢ t : T _{2}}{Γ ⊢ λ x : T _{1} . t : T _{1} \to T _{2}}$

它可以被读成：

假设 $T_{1}$ 成立；
在这个假设下构造出 $T_{2}$ ；
因而得到一个从 $T_{1}$ 到 $T_{2}$ 的函数。

这和逻辑里证明蕴含的结构非常像：

假设前件成立；
在此基础上推出后件；
因而得到“前件蕴含后件”。

最经典的例子是恒等函数：

$λ x : A . x : A \to A$

它对应逻辑中的平凡命题：

$A \Rightarrow A$

不过这里仍要保持边界感：
Curry–Howard 对应不是一句“所有类型系统都等于逻辑系统”就能概括完的。它成立于特定的形式系统中，而且具体对应关系依赖于所选语言与逻辑。

所以把它当作一种非常重要的理论视角是合适的，但不应在入门阶段把它说得过满。

5.15 本章小结

这一章真正建立起来的，是一条完整链条：

程序可能卡住，而类型系统的目标是排除某类卡住状态。
类型判断写作 $Γ ⊢ t : T$ ，表示在某个环境下，项具有某种类型。
本章对象语言是以 STLC 为核心、加入 Bool 与 if 的最小扩展语言。
良类型项不等于“绝对正确”，但它们满足一个关键的安全保证。
这个安全保证通常被分解为：
- 进展性：不会卡住；
- 保持性：求值不破坏类型。
保持性之所以成立，核心之一在于第三章已经准备好的替换理论。

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

先用类型规则给项做静态分类，再用进展性与保持性说明：良类型程序不会落入被本系统禁止的坏状态。

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

Γ ⊢ t : T 到底是什么意思？
为什么 (App) 规则能防止“把布尔值当函数用”？
为什么“类型安全”要拆成进展性和保持性？

回看导航

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

回看第 3 章：重新确认自由变量、替换、变量捕获与 α-重命名，因为保持性与替换引理都建立在这套基础之上。
回看第 4 章：重新确认“值 / 范式 / 卡住”“小步语义 / 大步语义”的区别，因为类型安全正是建立在“程序如何前进”这层定义之上。
配合附录A：重点查看“类型判断”“类型环境”“进展性”“保持性”“类型安全”“替换引理”等条目。
配合附录B：重点确认 Γ ⊢ t : T、\vdash、函数类型箭头等记号。
若你准备继续读第 6 章，可以带着一个问题往下看：
- 当语言不只包含函数和布尔值，而开始加入积类型、和类型、递归类型、引用类型时，这套类型规则骨架会怎样扩展？

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

Γ ⊢ t : T 这类类型判断的基本读法；
类型规则、类型检查与语法制导之间的关系；
“类型安全 = 进展性 + 保持性”这条后续各章都会反复依赖的主线。

本章练习

构造推导树，证明： $f : Bool \to Bool, x : Bool ⊢ f x : Bool$
说明为什么下面这个项无法通过类型检查： $true (λ x : Bool . x)$
构造推导树，证明： $⊢ λ x : Bool . if x then false else true : Bool \to Bool$
用自然语言解释进展性和保持性的区别，并说明它们如何一起排除卡住状态。
试着说明为什么下面这个说法不准确：
“良类型程序一定不会出任何问题。”

下一章，我们会在 STLC 的基础上继续扩展语言，加入更丰富的类型构造，如积类型、和类型、递归类型和引用类型。到那时，你会看到：类型规则的基本思想并没有变，只是它所处理的语言构造变得越来越丰富。

Keyboard shortcuts

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