[] 类型安全：典范形式、进展与保型

Glomzzz
2026-10-10
About

1 先把命题写下来

“良类型的程序不会出错”这句话，米尔纳（Milner）在 1978 年说成 well-typed programs cannot go wrong。现在终于可以把它写成一个精确的命题了。“出错”在这门语言里的意思就是“受阻”（ [定义] 范式与受阻）。

1.1 [定义] 类型安全 [type-safety]

2026-10-10
Glomzzz

采用 [定义] 类型与类型判断的类型关系、 [定义] 多步归约的运行关系，以及 [定义] 范式与受阻的受阻判定。称这套语言规则是类型安全（type safety）的，如果对任意项 $𝑡$ 、 $𝑡^{'}$ 和类型 $𝑇$ ：若 $𝑡 : 𝑇$ 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 没有受阻。

注意这句话里的量词：对所有良类型的 $𝑡$ ，对所有它能多步归约到的 $𝑡^{'}$ 。这正是 [例] 量词的范围提醒过的地方，写成符号以后，范围就不会有歧义。

直接证这个命题不好下手，因为 $⟶^{*}$ 可以归约任意多步。赖特（Wright）与费莱森（Felleisen）在 1994 年给出的办法，是把它拆成两条只涉及一步的定理：

进展（progress）：良类型的项要么是值，要么还能一步归约。它保证“现在不受阻”。
保型（preservation，也叫 subject reduction）：良类型的项一步归约，得到的项类型不变。它保证“归约一步以后，进展还能接着用”。

两条缺一不可。 [例] 归约到受阻里的 $succ (if true then false else 0)$ 现在能归约，一步归约之后就受阻了。只有进展，挡不住这种情况；只有保型，挡不住一开始就受阻的项。（这个例子本身没有类型，所以它不是两条定理的反例，只是说明为什么两条都需要。）

2 典范形式

证明进展时需要知道：某个类型的值长什么样。

2.1 [引理] 典范形式（canonical forms） [canonical-forms]

2026-10-10
Glomzzz

值与数值使用 [定义] 值与数值的定义，类型关系使用 [定义] 类型与类型判断。

若 $𝑣$ 是值且 $𝑣 : Bool$ ，则 $𝑣$ 是 $true$ 或 $false$ 。
若 $𝑣$ 是值且 $𝑣 : Nat$ ，则 $𝑣$ 是数值。

证明

由 [定义] 值与数值，值只有三种形状： $true$ 、 $false$ 、数值。

若 $𝑣$ 是数值，它是 $0$ （由 [引理] 反演第 1 条，类型只能是 $Nat$ ）或（由第 3 条，类型只能是 $Nat$ ）。由 [定理] 类型唯一，它不可能同时是 $Bool$ 。所以类型为 $Bool$ 的值只能是另两种。
同理，由 [引理] 反演第 1 条， $true$ 、 $false$ 的类型只能是 $Bool$ ，所以类型为 $Nat$ 的值只能是数值。

∎

这条引理是静态和动态之间的一座桥：左边是类型的信息（不运行就知道的），右边是形状的信息（运行时真正看到的）。进展的证明需要靠它把“条件是 $Bool$ 类型的值”变成“条件确实是 $true$ 或 $false$ ”，才能选择 E-IfTrue 或 E-IfFalse。若随意加上 $0 : Bool$ 而保持求值规则不变， $if 0 then true else false$ 就会被定型却受阻：静态分类不再保证运算要求的运行时形状。动态语言在运算时做的种类检查，正是在现场检查这类形状条件。

2.2 [附注] 静态类型与动态类型 [static-and-dynamic-typing]

2026-10-10
Glomzzz

“静态”（static）指不运行程序就能知道的东西，“动态”（dynamic）指运行时才能看到的东西。按类型检查发生在什么时候，程序语言大致分成两类：

静态类型语言（statically typed）：在运行之前检查类型，通常在编译阶段完成；不通过检查的程序被拒绝。Rust、Haskell、OCaml、Java、C 都属于这一类。 [定义] 类型与类型判断的类型系统也是： $𝑡 : 𝑇$ 只看项的形状，不执行 [定义] 一步归约的 $⟶$ 归约。
动态类型语言（dynamically typed）：程序先运行，每次真正做运算时再检查参与运算的值是不是合适的种类，不合适就抛出错误。Python、JavaScript、Ruby 属于这一类。

用 [定义] 项的集合的布尔值／自然数语言作类比，一种动态检查的设计是不预先构造 $𝑡 : 𝑇$ 的推导，而是在 $⟶$ 里给不合适的运行时操作补上报错规则（ [附注] 显式错误规则与 Kotlin 的底类型），把受阻换成可预期的异常。另一种操作可以采用转换规则（ [例] JavaScript 隐式转换与相等三角图）。真实语言往往同时有这两类处理；JavaScript 的条件还会采用真假值转换，不要求参数字面上就是布尔值。

对这门小语言的运算，类型规则、 [引理] 典范形式（canonical forms）与 [定理] 保型合起来保证：参数若被要求为 $Nat$ ，求值为值时就一定是数值，所以不必再检查它是否为布尔值。这不等于真实静态类型语言可以省掉所有运行时检查；例如 Kotlin 仍会抛出数组越界异常，Rust 的数组索引也可能需要边界检查。两者的取舍是：静态检查更早排除它所覆盖的错误，但会拒绝一些实际运行不会出错的程序（ [附注] 类型系统是保守的）；动态检查更灵活，但错误通常要等到运行到那一行才暴露。

另外，“静态 / 动态”和“强 / 弱”是两个不同的维度。C 是静态类型，但允许随意强制转换指针，类型系统不可靠；Python 是动态类型，但不会把字符串当整数用。 [推论] 类型安全证明的“类型安全”，指的是这套静态类型系统对受阻错误的可靠性，不是由“强／弱”这一称呼作出的保证。

对这个话题感兴趣的可以看看帝球的类型 vs. 类型检查

3 进展

进展回答的是“类型检查通过以后，下一步会不会无规则可用”。没有它，检查器即使给出了类型，也未必挡住 $succ true$ 这样的错误。具体地，若把 T-Succ 的前提错误地放宽成 $𝑡_{1} : Bool$ ，这个项就会被赋予 $Nat$ ，却既不是值也不能归约。进展还必须允许“已经是值”这个分支，否则 $0$ 这种合法结果反而会被误判为失败。对于有异常的真实语言，则要先明确哪些异常是许可的结果，不能把本文的进展原封不动当作“永不抛异常”。

3.1 [定理] 进展 [progress]

2026-10-10
Glomzzz

采用 [定义] 类型与类型判断的类型关系、 [定义] 值与数值的值定义，以及 [定义] 一步归约的归约关系。若 $𝑡 : 𝑇$ ，则 $𝑡$ 是值，或存在 $𝑡^{'}$ 使 $𝑡 ⟶ 𝑡^{'}$ 。

证明

对 $𝑡 : 𝑇$ 的推导归纳（类型推导版本的 [定理] 对推导归纳），按最后一步的规则分情形。

T-True、T-False、T-Zero： $𝑡$ 是值。
T-If： $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，前提里有 $𝑡_{1} : Bool$ 。对 $𝑡_{1}$ 用归纳假设：
- 若 $𝑡_{1}$ 能归约，用 E-If， $𝑡$ 也能归约；
- 若 $𝑡_{1}$ 是值，由 [引理] 典范形式（canonical forms）第 1 条，它是 $true$ 或 $false$ ，分别用 E-IfTrue、E-IfFalse。
T-Succ：前提 $𝑡_{1} : Nat$ 。若 $𝑡_{1}$ 能归约，用 E-Succ。若 $𝑡_{1}$ 是值，由 [引理] 典范形式（canonical forms）第 2 条它是数值，于是本身也是数值，因而是值。
T-Pred：前提 $𝑡_{1} : Nat$ 。若 $𝑡_{1}$ 能归约，用 E-Pred。若 $𝑡_{1}$ 是值，它是数值：是 $0$ 就用 E-PredZero；否则形如，用 E-PredSucc。
T-IsZero：与 T-Pred 相同，分别用 E-IsZero、E-IsZeroZero、E-IsZeroSucc。

∎

3.2 [例] 进展 [progress]

2026-10-10
Glomzzz

采用 [定义] 类型与类型判断的类型规则和 [定义] 一步归约的求值规则。取良类型的项 $𝑡 = pred (if false then 0 else succ 0) : Nat$ ，跟着 [定理] 进展的证明走一遍：

$𝑡$ 的推导最后一步是 T-Pred，前提 $if false then 0 else succ 0 : Nat$ 。对这个子项用归纳假设。
子项的推导最后一步是 T-If，前提里有 $false : Bool$ 。 $false$ 是值，由 [引理] 典范形式（canonical forms）它是 $true$ 或 $false$ ，这里是 $false$ ，于是用 E-IfFalse：子项 $⟶ succ 0$ 。
回到 $𝑡$ ：子项能归约，所以用 E-Pred， $𝑡 ⟶ pred (succ 0)$ 。

证明不只说“能归约”，还构造出了这一步的推导。对 $pred (succ 0)$ 再用一次进展：子项 $succ 0$ 是值，由 [引理] 典范形式（canonical forms）它是数值，且形如，于是用 E-PredSucc 得到 $0$ 。对 $0$ 再用一次进展：它是值，停止。

看 $succ true$ 为什么会受阻，再对照证明：要让它不受阻，要么 $true$ 能归约，要么 $true$ 是数值，两者都不成立。证明之所以没遇到这个麻烦，是因为 T-Succ 要求 $𝑡_{1} : Nat$ ，再经由典范形式把 $𝑡_{1}$ 限定为数值。类型系统正是在这里把坏程序挡在门外的。

4 保型

进展只能保证当前状态能运行，保型则让这个保证在运行后仍然可用。若修改 E-PredZero 为 $pred 0 ⟶ true$ ，原有类型规则仍会给 $succ (pred 0)$ 类型 $Nat$ ，第一步也可以执行；但它会变成没有类型、且受阻的 $succ true$ 。所以一次正确的类型检查必须能跨越每次运行时改写，不能“第一步安全就算安全”。编译器的优化、解释器的执行规则也要维持相应的不变量，否则即使前端检查器正确，后端仍能制造坏状态。

4.1 [定理] 保型 [preservation]

2026-10-10
Glomzzz

采用 [定义] 类型与类型判断的类型关系和 [定义] 一步归约的归约关系。若 $𝑡 : 𝑇$ 且 $𝑡 ⟶ 𝑡^{'}$ ，则 $𝑡^{'} : 𝑇$ 。

证明

对 $𝑡 ⟶ 𝑡^{'}$ 的推导归纳（ [定理] 对推导归纳），对 $𝑇$ 一般化。每个情形先对 $𝑡 : 𝑇$ 使用 [引理] 反演。

E-IfTrue： $𝑡 = if true then 𝑡_{2} else 𝑡_{3}$ ， $𝑡^{'} = 𝑡_{2}$ 。反演得 $𝑡_{2} : 𝑇$ 。
E-IfFalse：对称，反演得 $𝑡_{3} : 𝑇$ 。
E-If： $𝑡^{'} = if 𝑡_{1^{'}} then 𝑡_{2} else 𝑡_{3}$ ，前提 $𝑡_{1} ⟶ 𝑡_{1^{'}}$ 。反演得 $𝑡_{1} : Bool$ ， $𝑡_{2} : 𝑇$ ， $𝑡_{3} : 𝑇$ 。对前提用归纳假设（取类型为 $Bool$ ）得 $𝑡_{1^{'}} : Bool$ ，再用 T-If。
E-Succ：反演得 $𝑇 = Nat$ ， $𝑡_{1} : Nat$ 。归纳假设给出 $𝑡_{1^{'}} : Nat$ ，用 T-Succ。
E-PredZero： $𝑡^{'} = 0$ 。反演得 $𝑇 = Nat$ ，用 T-Zero。
E-PredSucc：，。反演两次：先得 $𝑇 = Nat$ 且，再得。
E-Pred：同 E-Succ，最后用 T-Pred。
E-IsZeroZero、E-IsZeroSucc： $𝑡^{'}$ 是 $true$ 或 $false$ 。反演得 $𝑇 = Bool$ ，用 T-True 或 T-False。
E-IsZero：反演得 $𝑇 = Bool$ ， $𝑡_{1} : Nat$ 。归纳假设给出 $𝑡_{1^{'}} : Nat$ ，用 T-IsZero。

∎

4.2 [例] 保型 [preservation]

2026-10-10
Glomzzz

对 [例] 多步归约到值的归约链，按 [定义] 类型与类型判断在每一项旁边写上类型。归约关系使用 [定义] 一步归约，保型性质及其证明见 [定理] 保型：

$\begin{matrix} if (iszero (pred (succ 0))) then succ 0 else 0 & : Nat \\ ⟶ & if (iszero 0) then succ 0 else 0 & : Nat \\ ⟶ & if true then succ 0 else 0 & : Nat \\ ⟶ & succ 0 & : Nat \end{matrix}$

类型始终是 $Nat$ 。以第一步为例看保型的证明怎样工作：这一步的推导是 E-If，前提是 $iszero (pred (succ 0)) ⟶ iszero 0$ 。由 [引理] 反演对 $𝑡 : Nat$ 反演，得到条件 $: Bool$ 、两个分支 $: Nat$ ；对前提用归纳假设（取类型 $Bool$ ），得到 $iszero 0 : Bool$ ；两个分支原封不动，再用 T-If 拼回去，得到新项 $: Nat$ 。

注意项本身变了很多，从一个 $if$ 变成了 $succ 0$ ，但类型这个“静态描述”一直成立。保型说的就是：运行不会让类型说过的话失效。

4.3 [附注] 为什么要“对

𝑇

一般化” [generalizing-the-type-in-preservation-proofs]

2026-10-10
Glomzzz

在 [定理] 保型的证明中，E-If 是 [定义] 一步归约的条件归约规则，类型关系采用 [定义] 类型与类型判断。处理这个情形时，归纳假设用在 $𝑡_{1}$ 上，而 $𝑡_{1}$ 的类型是 $Bool$ ，不一定是 $𝑡$ 的类型 $𝑇$ 。如果要证的性质写成“对这个固定的 $𝑇$ ， $𝑡^{'} : 𝑇$ ”，归纳假设就只能谈论这个 $𝑇$ ，在这里用不上。所以要证的性质必须写成“对任意 $𝑇$ ，若 $𝑡 : 𝑇$ 则 $𝑡^{'} : 𝑇$ ”。这个细节在自然语言的证明里很容易被略过， [定理] 确定性的证明里对 $𝑡^{″}$ 也做了同样的处理。

5 合起来

下面的推论把“当前不受阻”和“下一项仍有类型”接成对任意有限运行前缀的保证。只证明进展而不证明保型，保证可能一步后失效；只证明保型而不证明进展，则一个起初就受阻的良类型项没有任何一步可走，保型的条件从未成立，不能排除它。这个推论保证的是本文定义的“不受阻”，不保证程序一定终止，也不保证业务逻辑正确，例如得到 $false$ 是否符合程序员的意图。

5.1 [推论] 类型安全 [type-safety]

2026-10-10
Glomzzz

由 [定义] 项的集合、 [定义] 一步归约与 [定义] 类型与类型判断规定的布尔值／自然数语言是类型安全的（ [定义] 类型安全）：若 $𝑡 : 𝑇$ 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 没有受阻。

证明

对 $𝑡 ⟶^{*} 𝑡^{'}$ 的步数归纳（ [定义] 多步归约的两条规则）。

零步： $𝑡^{'} = 𝑡$ ，于是 $𝑡^{'} : 𝑇$ 。
至少一步： $𝑡 ⟶ 𝑡_{1}$ 且 $𝑡_{1} ⟶^{*} 𝑡^{'}$ 。由 [定理] 保型， $𝑡_{1} : 𝑇$ ；对 $𝑡_{1}$ 用归纳假设即可。

归纳给出的其实是更强的结论： $𝑡^{'} : 𝑇$ 。最后对 $𝑡^{'}$ 用 [定理] 进展：它是值或能归约，总之不是受阻的。

∎

5.2 [注记] 约定与必然 [convention-and-necessity]

2026-10-10
Glomzzz

[推论] 类型安全的证明里，我们一次也没有运行程序，却得到了关于所有运行的结论。这让人想起康德（Kant）的问题：有没有不靠经验、却又对经验有效的知识？

这里的答案相当朴素。结论之所以不靠“试”，是因为“运行”本身就是我们用规则定义出来的（ [定义] 一步归约），定理只是把定义里已经包含的东西展开。按逻辑实证主义的说法，这类命题是分析的：它的真依赖于定义。但这不等于它空洞。“所有良类型程序都不受阻”在定义里并不显眼，要靠反演、典范形式、两层归纳才能抽出来，中途还可能发现定义写错了（ [附注] 分支顺序里藏着证明和 [附注] 为什么 E-PredSucc 要求就是例子）。弗雷格说过，一个结论可以“像植物包含在种子里那样”包含在定义中，而不是“像梁木包含在房子里那样”一眼可见。

另一面是：证明只对这套规则成立。真实的 CPU 是否忠实地执行了这些规则，是另一个问题，属于经验，要靠测试和工程去回答。

6 练习：类型安全

本节练习（4题）

练习5.1：把进展与保型放到同一条链上

对

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

写出归约链与每站类型。逐步说明 [定理] 进展在哪里提供后继， [定理] 保型又怎样重建类型；第一步内部用到的类型为何不都是整项的

Nat

？

提示

每个中间项都为

Nat

；条件内部先保持

Nat

，外层

iszero

保持

Bool

，不能把这两个类型混成一个固定的

𝑇

。

参考答案

$\begin{matrix} if (iszero (pred (succ 0))) then pred 0 else succ 0 & : Nat \\ ⟶ & if (iszero 0) then pred 0 else succ 0 & : Nat \\ ⟶ & if true then pred 0 else succ 0 & : Nat \\ ⟶ & pred 0 & : Nat \\ ⟶ & 0 & : Nat \end{matrix}$

四步依次用 E-If + E-IsZero + E-PredSucc，E-If + E-IsZeroZero，E-IfTrue，E-PredZero。每个非末项都展示了进展要求的一个后继，末项 $0$ 展示了“已经是值”的分支。

第一步内层 $pred (succ 0)$ 从 $Nat$ 保持为 $0 : Nat$ ，T-IsZero 重建条件的 $Bool$ ，T-If 再和两个 $Nat$ 分支重建整项的 $Nat$ 。第二步条件变成 $true : Bool$ ，分支不变；第三步选出的 $pred 0$ 本来就在 T-If 的前提里具有 $Nat$ ；第四步由 T-Zero 得 $0 : Nat$ 。这才是类型为何保持的逐步解释，不只是把相同的标签写在每一行旁边。