[] 类型：语法导向、反演与唯一性

Glomzzz
2026-10-10
About

1 类型判断

1.1 [定义] 类型与类型判断 [types-and-typing-judgments]

2026-10-10
Glomzzz

设 $𝑡$ 是 [定义] 项的集合中的项。类型（type）只有两种： $𝑇 ⩴ Bool | Nat$ ，分别对应布尔值和自然数。类型判断（typing judgment） $𝑡 : 𝑇$ 读作“ $𝑡$ 具有类型 $𝑇$ ”，它是对下列七条规则封闭的最小关系。

横线上的判断是前提，横线下的是结论；没有前提的规则直接给出结论。 $𝑇$ 、 $𝑡_{1}$ 等符号按 [约定] 元变量代换，T-If 两个分支里的 $𝑇$ 必须代换成同一个类型。

1.2 [定义] 良类型 [well-typed-terms]

2026-10-10
Glomzzz

对 [定义] 类型与类型判断的类型关系，若存在某个类型 $𝑇$ ，使得 $𝑡 : 𝑇$ 有一棵由这些规则搭成的有限推导，就称项 $𝑡$ 是良类型的（well-typed）；否则称 $𝑡$ 是不良类型的（ill-typed）。

这个定义有三处值得逐一拆开：

“存在某个 $𝑇$ ”：良类型只要求有一个类型，不要求事先指定是哪一个。 $0$ 是良类型的，因为 $0 : Nat$ ；它不是 $Bool$ 并不影响这一点。
“有一棵推导”：和 $⟶$ 一样， $𝑡 : 𝑇$ 成立当且仅当能用 [定义] 类型与类型判断中七条规则的实例搭出一棵以它为根的有限树。所以说一个项良类型，就是说能写出这样一棵树；说它不良类型，就是说无论怎样搭都搭不出来。后者是一个关于所有可能推导的否定命题，不能仅凭尝试构造某棵推导树失败就断言它不良类型。要证明它不良类型，我们需要说明任何合法的推导都不可能成立。在这里，可以通过分析类型规则以及它们所要求的前提来完成证明，下面的例子会演示。
良类型是一个静态性质：在我们目前讨论的语言中， [定义] 类型与类型判断中的类型判断只依赖项的结构与类型规则，不需要执行 [定义] 一步归约中的 $⟶$ 归约。换句话说，我们不必运行一个项，就能判断它是否良类型。这正是静态类型检查（static type checking）的基础（与动态检查的对照见 [附注] 静态类型与动态类型）。不过，类型判断与求值虽然是两套不同的规则，它们之间是否协调一致，还需要通过 [推论] 类型安全的类型安全性定理来保证。

读法和 [定义] 一步归约完全一样：横线上是前提，横线下是结论， $𝑇$ 、 $𝑡_{1}$ 是元变量（ [约定] 元变量）。所以“对类型推导归纳”也照样成立，证明与 [定理] 对推导归纳相同，不再重复。

1.3 [例] 良类型与不良类型 [well-typed-and-ill-typed-terms]

2026-10-10
Glomzzz

使用 [定义] 类型与类型判断的七条类型规则，良类型与不良类型的含义见 [定义] 良类型。

良类型的例子。要说明 $if (iszero 0) then succ 0 else 0 : Nat$ ，从结论往上搭推导：

项的最外层是 $if$ ，结论形如 $if \dots : 𝑇$ 的规则只有 T-If。取 $𝑇 = Nat$ ，它要求三个前提： $iszero 0 : Bool$ 、 $succ 0 : Nat$ 、 $0 : Nat$ 。
第一个前提 $iszero 0 : Bool$ ：只有 T-IsZero 的结论形如 $iszero \dots$ ，结论类型恰好是 $Bool$ ，它要求 $0 : Nat$ 。T-Zero 给出这一点。
第二个前提 $succ 0 : Nat$ ：用 T-Succ，它要求 $0 : Nat$ ，再用 T-Zero。
第三个前提 $0 : Nat$ ：直接用 T-Zero。

每个前提都搭上了，合起来就是一棵完整的推导：

不良类型的例子。要说明 $succ true$ 没有类型，得证明对任何 $𝑇$ 都搭不出 $succ true : 𝑇$ 的推导。我们可以直接穷举七条规则：

结论左边形如 $succ \dots$ 的规则只有 T-Succ，其余六条的结论形状对不上，直接排除。所以如果有推导，最后一步只能是 T-Succ，此时 $𝑇 = Nat$ ，前提是 $true : Nat$ 。
再看 $true : Nat$ 。结论左边是 $true$ 的规则只有 T-True，而它的结论是 $true : Bool$ ，类型是 $Bool$ 不是 $Nat$ ，搭不上。没有别的规则可选。

唯一可能作为最后一步的 T-Succ 无法满足它的前提，因此不存在合法的推导树， $succ true$ 是不良类型的。

1.4 [附注] 不完整规格中的类型检查问题 [answers-to-incomplete-specification-questions]

2026-10-10
Glomzzz

采用 [定义] 类型与类型判断的七条规则， [例] 不完整的规格中的三个类型检查问题可以得到明确回答：

T-If 的三个前提都必须成立，所以 else 分支即使永远不执行也要检查。
两个分支的类型用的是同一个元变量 $𝑇$ ，所以“类型相同”就是字面相同，没有自动转换。
检查器拒绝 $𝑡$ ，意思是不存在 $𝑡 : 𝑇$ 的推导。具体是哪条规则的哪个前提搭不上，可以从搭建推导的过程中读出来，方法见 [附注] 从失败的推导里读出错误位置。

1.5 [附注] 从失败的推导里读出错误位置 [locating-errors-in-failed-typing-derivations]

2026-10-10
Glomzzz

为 [定义] 类型与类型判断中的类型判断寻找推导时，从要证的结论出发，选一条结论形状对得上的规则，再去搭它的每个前提。这七条规则是语法导向的，每种项形状只对应一条规则，见 [引理] 反演，所以每一步都只有一条规则可选，整个过程是一条确定的路径。路径断掉的地方，就是错误所在，它由三样东西确定：

位置：断在哪个子项上。搭推导时每进入一个前提，就进入了项的一个直接子项，所以断点对应语法树上的一个节点。
规则与前提：断点上方最后一次成功选用的规则，以及它的哪一个前提搭不上。
期望与实际：那个前提要求的类型，和子项实际能得到的类型。

以 $if true then 0 else (iszero 0)$ 为例。最外层选 T-If；第一个前提 $true : Bool$ 由 T-True 搭上；第二个前提要求 $0 : 𝑇$ ，T-Zero 给出 $𝑇 = Nat$ ；第三个前提于是要求 $iszero 0 : Nat$ ，但 T-IsZero 的结论类型是 $Bool$ 。断点因此是：T-If 的第三个前提，子项 $iszero 0$ ，期望 $Nat$ ，实际 $Bool$ 。编译器的报错信息“expected Nat Nat , found Bool Bool ”，内容就是这三样东西。

Rust 检查器 type_of type_of 在失败时只返回 None None ，把这些信息丢掉了。要保留它们，只需把返回类型从 Option<Type> Option<Type> 换成 Result<Type, Error> Result<Type, Error> ，在每个 ? ? 和比较失败处记下当时的规则、子项和两个类型。

1.6 [附注] 类型系统是保守的 [conservative-type-systems]

2026-10-10
Glomzzz

按 [定义] 一步归约的 E-IfTrue， $if true then 0 else false$ 运行一步就得到值 $0$ ，不会受阻；但 [定义] 类型与类型判断无法给它类型，因为 T-If 要求两个分支类型相同。这不是 bug。类型系统不运行程序，只看形状，它只能做近似。 [推论] 类型安全只保证一个方向：良类型的程序不受阻；它没有保证“不受阻的程序都良类型”。

2 反演：从结论倒推前提

先看这组规则的结论。每条规则的结论都形如“某个项 : 某个类型”，结论左边的项有一个最外层构造子（ $true$ 、 $if$ 、 $succ$ 等），这就是它的形状。把七条规则按结论左边的形状列出来：

项的形状	结论里出现这个形状的规则	条数
$true$	T-True	1
$false$	T-False	1
$0$	T-Zero	1
$if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$	T-If	1
$succ 𝑡_{1}$	T-Succ	1
$pred 𝑡_{1}$	T-Pred	1
$iszero 𝑡_{1}$	T-IsZero	1

“每种项的形状恰好出现在一条规则的结论里”指的就是这张表：第三列全是 $1$ 。既不是 $0$ （否则那种形状的项永远没有类型），也不大于 $1$ （否则同一个项可能有好几种定型方式）。这样的规则称为语法导向的（syntax-directed）：项的语法形状直接指定了该用哪条规则，不需要猜，也不需要回溯。

作为对照，下面两种情形都不是语法导向的：

如果再加一条规则 $\frac{𝑡 : Nat}{𝑡 : Bool}$ （“自然数可以当布尔值用”），它的结论左边是任意项 $𝑡$ ，不看形状。这时 $0 : Bool$ 可以由它推出， $0$ 这一行就有了两条规则可选。
如果把 T-If 拆成两条，一条要求条件是 $true$ ，一条要求条件是 $false$ ，那么 $if (iszero 0) \dots$ 这种条件不是常量的项就一条规则都没有，这一行变成 $0$ 。

语法导向带来一个很方便的推理方式：知道了 $𝑡 : 𝑇$ 成立，就能断定推导的最后一步用的是哪条规则，于是那条规则的前提也都成立。例如，知道 $succ 𝑡_{1} : 𝑇$ 成立，查表可知最后一步必然是 T-Succ，于是立刻得到 $𝑇 = Nat$ 且 $𝑡_{1} : Nat$ ，不用知道推导的其余细节。 [例] 良类型与不良类型里的两个例子也是这样做的：每一步都只有一条规则可选。

2.1 [引理] 反演 [typing-inversion]

2026-10-10
Glomzzz

以下结论只针对 [定义] 类型与类型判断的七条类型规则； $𝑡 : 𝑇$ 表示能由这些规则搭出有限推导， $Bool$ 、 $Nat$ 分别是布尔类型与自然数类型。

若 $true : 𝑇$ 或 $false : 𝑇$ ，则 $𝑇 = Bool$ 。若 $0 : 𝑇$ ，则 $𝑇 = Nat$ 。
若 $if 𝑡_{1} then 𝑡_{2} else 𝑡_{3} : 𝑇$ ，则 $𝑡_{1} : Bool$ ， $𝑡_{2} : 𝑇$ ， $𝑡_{3} : 𝑇$ 。
若 $succ 𝑡_{1} : 𝑇$ 或 $pred 𝑡_{1} : 𝑇$ ，则 $𝑇 = Nat$ 且 $𝑡_{1} : Nat$ 。
若 $iszero 𝑡_{1} : 𝑇$ ，则 $𝑇 = Bool$ 且 $𝑡_{1} : Nat$ 。

证明

每一条都看推导的最后一步。以第 3 条中的

succ

为例：七条规则里，结论左边形如

succ 𝑡_{1}

的只有 T-Succ。所以推导的最后一步就是 T-Succ，它的结论类型是

Nat

，前提是

𝑡_{1} : Nat

。其余各条同理，每次都只有一条规则可能适用。

∎

反演看起来平淡无奇，却是后面所有证明的发动机。它把“存在一棵推导”这种不知道细节的事实，拆成关于子项的具体信息。保型证明例如从开始，必须先知道 $𝑇 = Nat$ 、，再继续取出，才能证明删去外层构造以后类型还在。没有反演，就不能凭外观擅自断言子项有哪些类型；增加子类型规则时这个推理尤其需要重证，下面的附注会给出原因。

2.2 [附注] 反演依赖语法导向 [inversion-and-syntax-directed-rules]

2026-10-10
Glomzzz

[引理] 反演的逐形状证明依赖 [定义] 类型与类型判断的语法导向性：每种项形状只对应一条规则。如果将来加一条不看项形状的规则（例如子类型里常见的“若 $𝑡 : 𝑆$ 且 $𝑆$ 是 $𝑇$ 的子类型，则 $𝑡 : 𝑇$ ”），那么 $succ 𝑡_{1} : 𝑇$ 的最后一步就可能是这条新规则，“最后一步必然是 T-Succ”的推理就断了。到那时反演需要重新陈述、重新证明。

语法导向并不单凭“每种形状只有一条规则”就让输出类型自动唯一：T-If 的 $𝑇$ 还要从分支中确定。下面的定理补上这个保证，说明 type_of type_of 可以忠实地返回一个类型，而不必返回类型集合。没有唯一性，单个返回值可能只挑出了众多类型之一。例如带子类型的 Kotlin 中，一个 Int Int 表达式也可以出现在需要 Number Number 或 Any Any 的位置；那样的系统通常要另外区分推断出的类型和它能被接受为的所有类型，不能照搬本文的结论。

2.3 [定理] 类型唯一 [uniqueness-of-types]

2026-10-10
Glomzzz

对 [定义] 类型与类型判断的七条类型规则，若 $𝑡 : 𝑇$ 且 $𝑡 : 𝑇^{'}$ ，则 $𝑇 = 𝑇^{'}$ 。

证明

对 $𝑡$ 结构归纳（ [约定] 归纳证明的写法），对 $𝑇$ 、 $𝑇^{'}$ 一般化。

常量、 $succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ ：由 [引理] 反演，类型被项的形状直接定死（ $Bool$ 或 $Nat$ ），所以 $𝑇 = 𝑇^{'}$ 。
$if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ：由 [引理] 反演第 2 条， $𝑡_{2} : 𝑇$ 且 $𝑡_{2} : 𝑇^{'}$ 。 $𝑡_{2}$ 是直接子项，由归纳假设 $𝑇 = 𝑇^{'}$ 。

∎

3 练习：类型

本节练习（4题）

练习4.1：从结论搭起一棵类型推导

为

if (iszero (pred (succ 0))) then succ 0 else pred 0

写出完整的类型推导树，并指出推导中有没有哪一步需要先运行这个项。使用 [定义] 类型与类型判断。

提示

最外层用 T-If；条件从 T-IsZero 开始，两个分支都应得到

Nat

。

参考答案

每个叶子都是 T-Zero，两个分支具有同一个类型 $Nat$ 。定型过程中没有执行任何 $⟶$ 归约；条件最后会变成什么，不是搭这棵推导的前提。

练习4.2：证明没有类型，而不是只说“检查失败”

证明以下三项对任何

𝑇

都不能得到

𝑡 : 𝑇

：

succ (if true then 0 else false)

、

if (pred 0) then 0 else 0

、

iszero (iszero 0)

。每项给出无法满足的具体前提；其中有没有一项实际能归约到值？

提示

先用 [引理] 反演固定最后一条规则，再追到无法成立的前提。

参考答案

$succ (if true then 0 else false)$ 若有类型，最后只能用 T-Succ，要求内部 $if$ 为 $Nat$ 。T-If 随即要求 $false : Nat$ ，与 T-False 的结论不符。
$if (pred 0) then 0 else 0$ 若有类型，T-If 要求条件为 $Bool$ ，但 $pred 0$ 的类型只能是 $Nat$ 。
$iszero (iszero 0)$ 若有类型，外层 T-IsZero 要求内层为 $Nat$ ，但内层 T-IsZero 的结论只能是 $Bool$ 。