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

Glomzzz
2026-10-10
About

定义算术语言的类型判断与良类型词项，利用语法导向性质证明类型反演与类型唯一性．

1 类型判断

类型系统是在词项的抽象语法上定义的一组规则；它说明哪些词项与类型之间的关系可以成立．先区分三个概念：类型关系是词项与类型之间的关系， 类型判断是形如 $⊢ 𝑡 : 𝑇$ 的陈述， 类型规则则规定怎样证明这样的判断．

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

2026-10-10
Glomzzz

设 $𝑡$ 是词项的集合中的词项．类型的语法为 $𝑇 ⩴ Bool | Nat$ ，分别表示布尔类型与自然数类型．词项与类型是不同的语法类别，类型系统定义的是它们之间的关系．

类型关系由下面七条类型规则归纳定义：它是对这些规则封闭的最小关系． 类型判断 $⊢ 𝑡 : 𝑇$ 读作“可以由类型规则推出词项 $𝑡$ 具有类型 $𝑇$ ”；判断成立，当且仅当存在以它为结论的有限推导．

推导符号 $⊢$ 属于元语言，用来标记可推导性，与词项构造子或求值符号无关．含变量的语言通常写作 $Γ ⊢ 𝑡 : 𝑇$ ，读作“在语境 $Γ$ 中，词项 $𝑡$ 具有类型 $𝑇$ ”． $Γ$ 也称类型环境，记录作用域内变量的类型假设； $⊢$ 把这些假设与待证陈述分开．词项的集合的算术语言没有变量，所以采用空语境，并省略 $Γ$ ．为简洁起见，讨论这套规则时， $𝑡 : 𝑇$ 是 $⊢ 𝑡 : 𝑇$ 的简写．

横线上的判断是前提，横线下的是结论；没有前提的规则称为公理，仍是推导规则的特例． $𝑇$ 、 $𝑡_{1}$ 等符号按元变量代换： $𝑇$ 只能取类型， $𝑡_{1}$ 只能取词项； T-If 两个分支里的 $𝑇$ 必须代换成同一个类型．

T-True：前提无；结论 ⊢ true : Bool T-False：前提无；结论 ⊢ false : Bool T-Zero：前提无；结论 ⊢ 0 : Nat

T-If：前提 ⊢ t_(1) : Bool；⊢ t_(2) : T；⊢ t_(3) : T；结论 ⊢ if t_(1) then t_(2) else t_(3) : T

T-Succ：前提 ⊢ t_(1) : Nat；结论 ⊢ succ t_(1) : Nat T-Pred：前提 ⊢ t_(1) : Nat；结论 ⊢ pred t_(1) : Nat T-IsZero：前提 ⊢ t_(1) : Nat；结论 ⊢ iszero t_(1) : Bool

Definition 1.2 良类型 [well-typed-terms]

2026-10-10
Glomzzz

对类型与类型判断的类型关系，若存在某个类型 $𝑇$ ，使得 $𝑡 : 𝑇$ 有一棵由这些规则搭成的有限推导，则称词项 $𝑡$ 是良类型的；否则称 $𝑡$ 是不良类型的．

这个定义首先强调“存在某个 $𝑇$ ”：良类型只要求有一个类型，不要求事先指定是哪一个； $0$ 满足 $0 : Nat$ ，因此是良类型的（它不具有 $Bool$ 并不影响这一点）．这里固定的是项，寻找的是类型；类型居留性反过来固定类型，问是否存在具有该类型的项（三种问题的区分与常见误解见类型检查、类型推理与类型居留性）．

同时，它要求“有一棵推导”：和 $⟶$ 一样， $𝑡 : 𝑇$ 成立当且仅当能用类型与类型判断中七条规则的实例搭出一棵以它为根的有限树．说词项良类型，就是说能写出这样一棵树；说它不良类型，就是说无论怎样搭都搭不出来．后者是关于所有可能推导的否定命题，不能仅凭尝试构造某棵推导树失败就断言它不良类型；要证明它不良类型，需要分析类型规则及其前提，排除任何合法推导成立的可能（下面的例子会演示这一点）．

此外，良类型属于静态性质：在目前讨论的语言中，类型与类型判断中的类型判断只依赖项的结构与类型规则，无需执行一步规约中的 $⟶$ 规约．因此不必运行词项就能判断它是否良类型，这构成了静态类型检查的基础（与动态检查的对照见静态类型与动态类型）．至于类型判断与求值这两套规则之间是否协调一致，还要靠类型安全的类型安全定理来保证．

规则的读法与一步规约相同：横线上是前提，横线下是结论， $𝑇$ 、 $𝑡_{1}$ 是元变量（元变量）．这里还要注意类型与词项是不同的语法类别： $𝑇$ 只能代换为 $Bool$ 或 $Nat$ ， $𝑡_{1}$ 则代换为词项． T-If 的两个分支可以同为 $Bool$ 或同为 $Nat$ ，但同一次规则应用中的 $𝑇$ 必须取同一个类型．

类型规则同样是归纳定义，因此也可以对类型推导使用规则归纳法，原理与规则归纳法相同．这种横线上写前提、横线下写结论的记号来自形式逻辑，与自然演绎相近，直接刻画判断的可推导性（至于检查器按什么顺序执行，还需另行规定）．

Example 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（结论类型恰好是 $Bool$ ），再由 T-Zero 满足其前提 $0 : Nat$ ；第二个前提 $succ 0 : Nat$ 用 T-Succ，再接 T-Zero；第三个前提 $0 : Nat$ 直接用 T-Zero．每个前提都搭上了，合起来就是完整的推导：

T-If：前提 [T-IsZero：前提 [T-Zero：前提 [无]；结论 0 : Nat]；结论 iszero 0 : Bool；T-Succ：前提 [T-Zero：前提 [无]；结论 0 : Nat]；结论 succ 0 : Nat；T-Zero：前提 [无]；结论 0 : Nat]；结论 if (iszero 0) then succ 0 else 0 : Nat

再看不良类型的例子．要说明 $succ true$ 没有类型，得证明对任何 $𝑇$ 都搭不出 $succ true : 𝑇$ 的推导．逐一检查七条规则：结论左边形如 $succ \dots$ 的规则只有 T-Succ，其余六条形状不符，直接排除；若存在推导，最后一步只能是 T-Succ，此时 $𝑇 = Nat$ ，且前提要求 $true : Nat$ ．再看 $true : Nat$ ，结论左边为 $true$ 的规则只有 T-True，但 T-True 给出的类型是 $Bool$ ，与所需的 $Nat$ 冲突，没有别的规则可选．唯一可能作为最后一步的 T-Succ 无法满足前提，因此不存在合法的推导树， $succ true$ 是不良类型的．

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

2026-10-10
Glomzzz

打开独立页面 →

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

2026-10-10
Glomzzz

打开独立页面 →

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

2026-10-10
Glomzzz

打开独立页面 →

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$ ：本文的每种项形状恰好对应一条候选定型规则．这组规则是语法导向的：可以依据项的语法形状确定应尝试哪条规则，不必猜测最后一步．一般来说，语法导向不要求每个项都有规则可选，更不保证规则的前提都成立；没有匹配规则或前提搭不上，都可能导致拒绝． Harper 在 Type Systems for Programming Languages §1.2 中的表述是“至多一条规则”，不要误解为“必须恰好只有一条”．

作为对照，如果再加一条规则 $\frac{𝑡 : Nat}{𝑡 : Bool}$ （“自然数可以当布尔值用”），它的结论左边是任意项 $𝑡$ ，不按项的形状限制．仅看 $0$ 的语法形状，既不能排除 T-Zero，也不能排除这条转换规则，最后一步不再由形状唯一决定．具体要推出 $0 : Bool$ 时，最后用的是转换规则，它的前提 $0 : Nat$ 再由 T-Zero 给出．

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

Lemma 2.1 反演 [typing-inversion]

2026-10-10
Glomzzz

这里的四条结论只针对类型与类型判断的七条类型规则； $𝑡 : 𝑇$ 表示能由这些规则搭出有限推导， $Bool$ 、 $Nat$ 分别是布尔类型与自然数类型．第 1 条，若 $true : 𝑇$ 或 $false : 𝑇$ ，则 $𝑇 = Bool$ ；若 $0 : 𝑇$ ，则 $𝑇 = Nat$ ．第 2 条，若 $if 𝑡_{1} then 𝑡_{2} else 𝑡_{3} : 𝑇$ ，则 $𝑡_{1} : Bool$ ， $𝑡_{2} : 𝑇$ ， $𝑡_{3} : 𝑇$ ．第 3 条，若 $succ 𝑡_{1} : 𝑇$ 或 $pred 𝑡_{1} : 𝑇$ ，则 $𝑇 = Nat$ 且 $𝑡_{1} : Nat$ ．第 4 条，若 $iszero 𝑡_{1} : 𝑇$ ，则 $𝑇 = Bool$ 且 $𝑡_{1} : Nat$ ．

Proof.

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

succ

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

succ 𝑡_{1}

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

Nat

，前提是

𝑡_{1} : Nat

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

∎

反演利用规则定义的最小关系，穷尽结论可能来自的规则，把“某个判断存在推导”拆成任何合法推导都必须满足的前提信息（这与直接把单条推导规则的蕴涵方向倒过来不同）．保型证明例如从 $pred (succ nv) : T$ 开始，必须先知道 $𝑇 = Nat$ 、 $succ nv : Nat$ ，再继续取出 $nv : Nat$ ，才能证明删去外层构造以后类型还在．没有反演，就不能凭外观擅自断言子项有哪些类型；增加子类型规则时这个推理尤其需要重证，下面的附注会给出原因．

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

2026-10-10
Glomzzz

打开独立页面 →

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

Theorem 2.3 类型唯一 [uniqueness-of-types]

2026-10-10
Glomzzz

对类型与类型判断的七条类型规则，若 $𝑡 : 𝑇$ 且 $𝑡 : 𝑇^{'}$ ，则 $𝑇 = 𝑇^{'}$ ．

Proof.

对

𝑡

结构归纳（归纳证明的写法），对

𝑇

、

𝑇^{'}

一般化．当

𝑡

是常量、

succ 𝑡_{1}

、

pred 𝑡_{1}

或

iszero 𝑡_{1}

时，由反演，类型由项的形状直接唯一确定为

Bool

或

Nat

，所以

𝑇 = 𝑇^{'}

．当

𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}

时，由反演第 2 条得

𝑡_{2} : 𝑇

且

𝑡_{2} : 𝑇^{'}

；

𝑡_{2}

是直接子项，由归纳假设得

𝑇 = 𝑇^{'}

．

∎

3 练习：类型

Exercises (4)

Exercise 4.1. 从结论搭起一棵类型推导

为

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

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

Hint

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

Nat

．

Solution

T-If：前提 [T-IsZero：前提 [T-Pred：前提 [T-Succ：前提 [T-Zero：前提 [无]；结论 0 : Nat]；结论 succ 0 : Nat]；结论 pred (succ 0) : Nat]；结论 iszero (pred (succ 0)) : Bool；T-Succ：前提 [T-Zero：前提 [无]；结论 0 : Nat]；结论 succ 0 : Nat；T-Pred：前提 [T-Zero：前提 [无]；结论 0 : Nat]；结论 pred 0 : Nat]；结论 if (iszero (pred (succ 0))) then succ 0 else pred 0 : Nat

每个叶子都是 T-Zero，两个分支具有同一个类型 $Nat$ ．定型过程中没有执行任何 $⟶$ 规约，搭这棵推导完全不依赖条件最终求值成什么．

Exercise 4.2. 严格证明项无类型

证明下面三项对任何

𝑇

都不能得到

𝑡 : 𝑇

：

succ (if true then 0 else false)

、

if (pred 0) then 0 else 0

、

iszero (iszero 0)

．每项给出无法满足的具体前提，并判断其中是否有实际能规约到值的项．

Hint

先用反演固定最后一条规则，再追到无法成立的前提．

Solution

若 $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$ ．

这三种分析排除了所有可能的最后规则，因此是不存在推导的严格证明．第一个项却可以规约到 $succ 0$ ：实际没有执行坏分支．这再次说明“不良类型”并不等于“这次运行必定出错”．

Exercise 4.3. 反演不需要看见整棵推导

设

𝑐

、

𝑡_{1}

、

𝑢

是任意项．已知

if 𝑐 then (pred (succ 𝑡_{1})) else 𝑢 : 𝑇

，但没有拿到它的推导树．说明此时仍能确定的

𝑇

、

𝑐

、

𝑡_{1}

、

𝑢

的类型信息，并逐次标明使用反演的哪一条．

Hint

先反演 T-If，再连续反演 T-Pred 和 T-Succ；整项的

𝑇

由其中一个分支确定．

Solution

T-If 给出 $𝑐 : Bool$ 、 $pred (succ 𝑡_{1}) : 𝑇$ 、 $𝑢 : 𝑇$ ． T-Pred 给出 $𝑇 = Nat$ 以及 $succ 𝑡_{1} : Nat$ ； T-Succ 再给出 $𝑡_{1} : Nat$ ．代回得到 $𝑢 : Nat$ ．

因而一定有 $𝑇 = Nat$ 、 $𝑐 : Bool$ 、 $𝑡_{1} : Nat$ 、 $𝑢 : Nat$ ．这只提取已有推导必须满足的前提，并没有假定 $𝑐$ 或 $𝑡_{1}$ 已经求值，也不需要猜原推导的其他细节．

Exercise 4.4. 扩展：增加转换规则的影响

只在类型规则中增加

\frac{𝑡 : Nat}{𝑡 : Bool}

，求值规则暂不改动．给出一个具有两个类型的项，指出原来的类型唯一、反演和语法导向分析各在哪一步失效．

Hint

保留七条旧规则，再添加“由

𝑡 : Nat

推出

𝑡 : Bool

”．首先检查

0

．

Solution

T-Zero 给出 $0 : Nat$ ，新规则再给出 $0 : Bool$ ，所以类型唯一不再成立．反演中“若 $0 : 𝑇$ ，则 $𝑇 = Nat$ ”也失效．

更根本地，新规则的结论左边是任意项，不由最外层形状唯一决定．现在 $0 : Bool$ 的推导最后一步来自新规则，因此原来的语法导向表和逐形状反演不能照搬．扩展语言改动了规则，需要重新陈述并检验相应性质（原定理针对未扩展语言，依然成立）．

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

References

Backlinks