第十章子结构类型系统

阅读提示

本章会频繁使用“结构规则（structural rules）”“线性 / 仿射 / 相关 / 有序”“环境分裂（context splitting）”“线性函数类型（linear function type）”等术语。若你在阅读时想快速回查定义与记号，建议配合：

附录A《术语表》中的 A.8“子结构类型系统相关术语”

附录B《符号速查表》中的“子结构类型系统相关记号”

前面的章节里，我们逐步建立了一条很熟悉的主线：

程序有语法；
程序按操作语义运行；
类型系统在运行之前限制哪些程序是被允许的；
类型安全说明这些限制确实能排除某类坏状态。

但到目前为止，我们默认了一个很强、也很容易被忽略的前提：

变量可以随便用。

也就是说，在常规类型系统中，一个变量通常可以：

不用；
用一次；
用很多次；
交换使用顺序。

对大多数纯函数程序来说，这没有问题。但一旦程序里出现“资源”概念，这种默认自由就会变得危险：

文件句柄不能关闭两次；
内存不能释放后继续使用；
锁必须按协议获取和释放；
通信通道中的消息必须按顺序发送和接收。

这正是子结构类型系统（substructural type systems）要处理的问题。它们的核心思想不是给值增加新的“形状类型”，而是进一步限制：

一个变量可以被使用几次，以及是否必须按某种顺序使用。

本章要回答的问题是：

常规类型系统默认允许了哪些结构规则？
禁止其中一部分之后，类型系统会发生什么变化？
为什么这会把“类型”从“描述值的形状”推进到“描述值的使用纪律”？

本章的写法分三层：

前半先建立资源使用纪律的直觉；
中间给出一个最小形式核心，说明子结构系统究竟改动了哪些判断规则；
后半再把这些思想和 Rust、Zig、会话类型等实践方向对照起来。

也就是说，本章不只是做语言评论，而是要把“结构规则如何进入类型判断系统”这件事说清楚。

这一章的目标，是把这种思想讲清楚。你会看到：

常规类型系统其实隐含允许若干结构规则；
子结构类型系统通过禁止其中一部分规则，控制资源使用方式；
线性类型、仿射类型、相关类型、有序类型，正是不同限制强度下的系统；
Rust 的所有权系统、会话类型等实践方向，都可以在这里找到理论影子。

10.1 常规类型系统里“默认允许”的东西

在 STLC 以及大多数常规类型系统中，类型环境通常写成：

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

然后类型判断写成：

$Γ ⊢ t : T$

表面上看，这只是“在某个环境下判断项的类型”。但实际上，这种写法通常默认了若干关于环境的结构性质。它们在逻辑里叫做结构规则（structural rules）。

10.1.1 交换（Exchange）

交换说的是：

环境中假设的顺序通常不重要。

如果你有：

$Γ_{1}, x : A, y : B, Γ_{2} ⊢ t : T$

那么通常也默认可以写成：

$Γ_{1}, y : B, x : A, Γ_{2} ⊢ t : T$

也就是说，x:A 和 y:B 的先后顺序不会影响判断。

10.1.2 弱化（Weakening）

弱化说的是：

允许在环境中加入一个根本没有用到的变量。

如果：

$Γ ⊢ t : T$

并且变量 x 不在 t 中自由出现，那么通常也允许：

$Γ, x : A ⊢ t : T$

这对应的直觉是：

你可以拥有一个资源；
但完全不使用它；
程序仍然是合法的。

10.1.3 收缩（Contraction）

收缩说的是：

如果同一个资源被写成两份，那么可以把它们合并，等价地理解为“这个变量可以重复使用”。

更准确地说，在逻辑里，收缩表达的是“同一假设可以被重复使用”。在类型系统直觉里，它对应：

一个变量可以被使用多次；
你不需要精确追踪它用了几次。

这条规则在资源语义里非常关键，因为它正是“复制使用”的来源。

10.2 为什么这些规则会出问题？

在纯函数式场景下，这些结构规则通常非常自然。

例如，给定一个普通整数变量 x：

你可以不用它；
也可以把它传给两个不同函数；
还可以交换它与别的变量在环境中的书写顺序。

这没有什么问题，因为整数不是“必须精确管理的一次性资源”。

但如果 x 表示的是文件句柄、数据库连接、锁、唯一所有权对象，那么情况就变了：

允许弱化：可能意味着“拿到了资源却忘记释放”；
允许收缩：可能意味着“同一个资源被复制使用，从而重复关闭、重复释放”；
允许交换：有时会破坏协议顺序，例如必须先发送再接收的通信过程。

所以子结构类型系统的出发点可以概括为：

不是所有值都应该像普通数学对象那样自由使用。

有些值代表资源，而资源的核心特征恰恰是：

使用次数受限；
使用顺序可能受限；
使用后状态发生变化。

10.3 子结构类型系统的总体图景

通过对交换、弱化、收缩三条规则做不同组合的保留与禁止，我们得到一系列不同系统。

系统	允许的结构规则	变量使用约束
常规（unrestricted）	Exchange + Weakening + Contraction	可不用、可用一次、可用多次，顺序无关
仿射（affine）	Exchange + Weakening	至多使用一次
相关（relevant）	Exchange + Contraction	至少使用一次
线性（linear）	Exchange	恰好使用一次
有序（ordered）	无	恰好使用一次，且按顺序使用

这张表值得仔细读。

先看一个最小对照：

维度	常规系统	线性系统
变量使用	可丢弃、可复制	不可丢弃、不可复制
应用规则	同一环境可同时给左右子项	环境必须分裂给左右子项
函数类型	`A -> B`	`A ⊸ B`
关注重点	值是什么形状	值怎样被使用

后面 10.4–10.6 节真正要说明的是：这些差异不是“解释口味不同”，而是会直接进入类型判断规则本身。

10.3.1 常规系统

常规类型系统允许：

不用变量（弱化）
多次使用变量（收缩）
调整环境顺序（交换）

这是最宽松的情形。

10.3.2 仿射系统

仿射系统禁止收缩，但保留弱化和交换。

因此：

变量可以不用；
但一旦用了，就不能再复制使用。

所以仿射变量满足：

至多使用一次。

10.3.3 相关系统

相关系统禁止弱化，但保留收缩和交换。

因此：

变量不能完全不用；
但可以使用多次。

所以相关变量满足：

至少使用一次。

10.3.4 线性系统

线性系统既禁止弱化，也禁止收缩，只保留交换。

因此：

变量不能丢掉；
也不能复制；
必须恰好使用一次。

这就是最经典的线性资源约束。

10.3.5 有序系统

有序系统连交换也不允许。

因此：

变量必须恰好使用一次；
而且必须按环境中给定的顺序使用。

这比线性更强，因为它不仅控制“用了几次”，还控制“按什么顺序用”。

10.4 线性类型：最经典的资源控制系统

线性类型系统是子结构类型系统中最核心的一类。它表达的约束非常明确：

每个线性变量必须恰好使用一次。

在进入例子之前，先给出一个最小形式核心。这样后面讲“环境分裂”“线性函数”“无限制值”时，就不会显得像零散技巧。

10.4.0 一个最小形式核心

在常规 STLC 中，我们写：

$Γ ⊢ t : A$

其中环境 Γ 默认允许交换、弱化、收缩。

而在线性系统里，一个常见的最小写法是把环境分成两部分：

$Γ; Δ ⊢ t : A$

其中：

Γ 放无限制假设（unrestricted assumptions），可自由复制、丢弃；
Δ 放线性假设（linear assumptions），必须被精确使用。

这不是唯一写法，但它最能表达本章主线：

子结构类型系统不是只改“解释”，而是直接改类型判断所允许的环境结构。

在这种最小骨架下，最典型的几条规则形状如下。

变量规则

无限制变量与线性变量通常分开处理：

$Γ , x : A ; \emptyset ⊢ x : A$

$Γ ; x : A ⊢ x : A$

直觉上：

若 x 是无限制变量，它不会消耗线性资源；
若 x 是线性变量，那么这一步正好把它用掉。

线性抽象规则

$\frac{Γ ; Δ , x : A ⊢ t : B}{Γ ; Δ ⊢ λ x . t : A ⊸ B}$

它表示：

若函数体在使用一次 x:A 的前提下得到 B；
那么这个函数本身就是一个线性函数 A ⊸ B。

普通抽象规则

$\frac{Γ , x : A ; Δ ⊢ t : B}{Γ ; Δ ⊢ λ x . t : A \to B}$

它表示：

若参数 x:A 被放在无限制环境中；
那么函数可以按普通方式使用这个参数，得到普通函数类型 A \to B。

这里先不追求完整系统，只抓住一个最重要的变化：

一旦环境被区分成“可自由使用的部分”和“必须精确使用的部分”，类型规则的形状就已经不同于常规 STLC。

10.4.1 为什么“恰好一次”有用？

考虑一个抽象的文件接口：

type file
val open  : string -> file
val read  : file -> string * file
val close : file -> unit

这里把 file 当成一种必须精确管理的资源。若没有线性约束，下面这些错误都很难通过普通类型系统排除：

close f; close f：重复关闭
close f; read f：关闭后继续使用
let _ = open "a.txt"：打开后丢失，不再关闭

线性类型的理想目标是：

打开资源后，必须用掉它；
用掉之后，旧变量失效；
不可能偷偷复制出第二份同一资源。

这正对应“恰好使用一次”的语义。

10.4.2 限定符：区分线性值和普通值

很多线性系统不会要求“所有东西都线性”，否则就太不实用了。更常见的做法是引入一个限定符（qualifier），区分：

线性值
无限制值

例如：

$q ::= t e x t l in mi d t e x t u n$

然后把类型写成带限定符的形式：

$q A$

其中：

lin A 表示线性地使用一个 A
un A 表示一个普通、可自由复制和丢弃的 A

这样：

文件句柄可以是 lin File
普通布尔值可以是 un Bool

这避免了“所有值都必须精确使用一次”的不现实要求。

这里也要补一个系统层面的提醒：

不同教材会用不同方式呈现“线性 / 无限制”的区分：有的把它写成限定符 lin / un，有的把它吸收到上下文分类或类型构造里。本章采用的是一种更适合入门的混合写法：同时区分两类值、两类环境和两类函数。

10.5 环境分裂：线性系统最关键的机制

线性类型系统里，最值得真正理解的机制是环境分裂（context splitting）。

为什么它重要？
因为一旦一个项有两个子项，类型系统就必须决定：

环境中的线性变量应该分给哪一边？

最典型的例子是函数应用：

$t_{1} t_{2}$

如果变量 x 是线性的，那么它不可能同时被 t_1 和 t_2 两边都使用。否则就相当于复制了一份线性资源。

于是在线性系统中，应用规则不再像 STLC 那样简单地把同一个环境同时给两个前提，而是要把环境拆成两部分。

这也是为什么前面 10.4.0 节要先把判断写成：

$Γ; Δ ⊢ t : A$

因为一旦进入应用，真正被“分裂”的通常是线性部分 Δ，而不是无限制部分 Γ。

10.5.1 线性应用规则的形状

一个典型的线性应用规则可以写成：

$\frac{Γ ; Δ _{1} ⊢ t _{1} : T _{1} ⊸ T _{2} Γ ; Δ _{2} ⊢ t _{2} : T _{1}}{Γ ; Δ _{1} \circ Δ _{2} ⊢ t _{1} t _{2} : T _{2}}$

这里：

$m u lt ima p$ 常用来表示线性函数类型；
$De lt a_{1} c i rc De lt a_{2}$ 表示两个线性环境之间的合法合并 / 分裂对应关系；
同一个无限制环境 Γ 可以同时出现在两边，而线性环境必须被精确拆分。

如果你更喜欢把所有环境都写成一个整体，也常会看到类似：

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

两种写法表达的是同一个核心思想：
线性资源不能被两个子推导共享。

核心直觉是：

t1 用一部分资源；
t2 用另一部分资源；
同一个线性变量不能出现在两边。

10.5.2 分裂规则的直觉

环境分裂通常满足如下原则：

无限制变量可以同时出现在两边；
线性变量只能分配给一边。

直觉上很像分配实物资源：

一本可复制的公开文档可以两边都拿到；
一张唯一的车票只能交给其中一方。

10.5.3 一个例子

设环境中有：

$x : un (A \to B), y : lin A$

要检查应用 x y。

x 是无限制的，因此可以出现在需要它的一侧，也不担心复制问题；
y 是线性的，因此必须只分给参数那一侧，不能再出现在函数那一侧。

所以环境大致分裂成：

左边给函数位置：x : un(A → B)
右边给参数位置：x : un(A → B), y : lin A
或者在某些系统里更严格地只给 y，取决于环境定义细节

真正重要的是：

线性变量不会被两个子推导共享。

这正是线性性得以维持的关键。

如果你想把这里的记号和前面章节统一起来，可以顺手对照：

附录A中的“环境分裂”“线性函数”“无限制值”条目；
附录B中的 A ⊸ B 与 Γ_1 \circ Γ_2 记号说明。

10.6 线性函数与无限制函数

在线性系统中，函数本身也常常分成不同种类。

这里最好把 10.4 节的最小形式核心和本节连起来看：
一旦系统同时区分

无限制环境与线性环境；
普通值与线性值；

函数类型也自然会分成“普通函数”和“线性函数”两类。否则，“参数到底能不能被复制或丢弃”这件事就无法进入类型本身。

10.6.1 线性函数

线性函数通常写成：

$A ⊸ B$

它表示：

函数接受一个线性使用的 A
并产生一个 B

直觉上，这个函数承诺：

不会偷偷复制它的参数；
也不会直接把参数丢掉不用。

10.6.2 普通函数

无限制函数则通常写成普通箭头：

$A t o B$

它允许：

参数被使用零次、一次或多次；
函数自身也可以自由复制使用。

因此，本章中的一个最小对照可以写成：

函数种类	记号	对参数的使用纪律
普通函数	`A -> B`	可丢弃、可复制
线性函数	`A ⊸ B`	必须恰好使用一次

这张表虽然很小，但抓住了子结构类型系统和常规函数类型系统最关键的差别之一。

10.6.3 为什么要区分两类函数？

因为“函数是否会复制 / 丢弃参数”本身就是资源语义的一部分。

例如：

恒等函数 λx.x 可以是线性的；
常函数 λx.c 会丢弃参数，因此不能被看成线性函数；
λx.(x, x) 会复制参数，也不能是线性函数。

所以在子结构类型系统里，函数类型不再只是“输入输出类型”的问题，还带着：

这个函数怎样使用它的参数？

10.7 仿射类型：至多使用一次

虽然线性类型很漂亮，但“恰好使用一次”在工程上有时过于严格。

因为现实程序里，某些值“最终没用到”并不一定是错误。
例如：

一个分支里提前返回；
一个对象构造出来后根据条件被直接丢弃；
某个资源由析构机制自动回收。

这时，仿射类型就变得更实用。

仿射系统保留弱化，但禁止收缩，因此：

仿射变量至多使用一次。

10.7.1 与线性类型的区别

线性与仿射的差别只有一个：

线性：必须使用一次
仿射：可以不用，但不能多次用

也就是说，仿射类型比线性类型宽松一点。

10.7.2 为什么仿射在实践中更常见？

因为很多编程场景里，“不用”比“复制”更容易安全处理。

如果一个资源没被使用，可以用析构、作用域结束、垃圾回收或其他机制统一处理；
但如果一个资源被复制成两份，再分别释放或修改，就更容易出错。

因此很多实际系统更愿意保留“可丢弃”，而重点禁止“可复制”。

10.8 相关类型：至少使用一次

相关类型（relevant types）走的是另一条路：

保留收缩；
禁止弱化。

于是变量必须至少被用一次，但可以用很多次。

这类系统在入门教材里不如线性和仿射常见，但它提供了一种有趣的资源视角：

你不能无视一个资源，但一旦开始使用，它可以重复使用。

这种思路适合表达某些“必须消费”或“必须响应”的约束，不过工程上使用得没有仿射和线性广泛。

10.9 有序类型：连顺序也要控制

如果连交换规则也去掉，就得到有序类型系统。

在本章的入门性概括里，可以先把它理解为：

每个变量恰好使用一次；
而且必须按环境给定顺序使用。

为什么会有人需要这种系统？
因为有些资源不是只关心“用没用、用了几次”，还关心：

有没有按正确顺序使用。

这里也要保留一点边界感：不同教材对 ordered / non-commutative 系统的具体形式化会更细，本章只抓住最核心的资源直觉——顺序本身也可能是类型系统要约束的对象。

这在通信协议中尤其明显。

10.9.1 一个协议直觉

假设某协议规定：

先发送用户名
再发送密码
最后等待登录结果

这里的问题不是“消息发送几次”，而是“顺序是否正确”。

如果你把第 2 步和第 1 步颠倒了，协议就坏了。
这说明某些程序性质天然具有顺序敏感性。

有序类型系统正是为这种顺序敏感资源提供形式基础。

10.10 Rust 的所有权系统：仿射思想的工程化

下面开始进入“理论与真实语言的对照”层。这里的目的不是评价某门语言优劣，而是说明：

资源安全可以通过不同语言设计路线实现，子结构类型只是其中一条重要路线。

子结构类型系统最著名的现实影响之一，就是 Rust 的所有权与借用系统。

当然，不能简单地说：

“Rust 就是线性类型系统” 或者 “Rust 就是仿射类型系统”

更准确的说法是：

Rust 的设计明显吸收了仿射 / 线性资源控制的核心思想，但它是一个更复杂的工程系统。

10.10.1 所有权移动的仿射直觉

在 Rust 中：

一个值通常有唯一所有者；
move 之后，旧绑定不能继续使用。

例如：

#![allow(unused)]
fn main() {
let s1 = String::from("hello");
let s2 = s1;
// println!("{}", s1); // 编译错误
}

这非常接近仿射直觉：

s1 表示的资源不能再被原绑定继续使用；
使用权被转移给了 s2；
资源不会被任意复制。

因此，Rust 中“默认按 move 使用的值”在直觉上很接近：

至多使用一次的资源。

10.10.2 为什么不能简单说“Rust = 仿射类型系统”？

因为 Rust 还包含很多额外机制：

借用（borrowing）
生命周期（lifetimes）
可变 / 不可变引用的区别
trait、析构、内部可变性等复杂设计

这些都超出了一个最小仿射 λ-演算的范围。

所以更稳妥的表述是：

Rust 以仿射资源使用为核心直觉，并在其上构造了完整的工程化内存与别名控制系统。

10.10.3 `&mut` 与线性直觉

Rust 的可变借用 &mut T 常常被拿来和线性使用作类比，因为：

同一时刻只能有一个活跃可变借用；
它体现了“独占访问”的思想。

但这仍然只是类比，而不是简单的同构。
因为 Rust 的借用系统还涉及时间范围、重借用、生命周期推理等问题，不能直接等同于教科书里的线性变量。

10.11 Zig 的对照：不走子结构类型这条路

如果说 Rust 代表了“把资源纪律尽可能前移到编译期”的一条路线，那么 Zig 更接近另一种设计取向：

保持语言机制相对直接；
不引入完整的所有权 / 借用静态系统；
把更多责任交给程序员和约定；
再辅以调试模式和运行时检查帮助发现错误。

因此，和 Rust 相比，Zig 并没有把“变量使用次数和别名纪律”上升为同样强的静态类型约束。

所以从子结构类型系统的角度看，更合适的说法是：

Zig 可以作为一个有趣的对照样本：它处理资源问题，但并不通过完整的线性 / 仿射类型系统来处理。

这一节的重点不是说“哪条路线更好”，而是帮助你看清：

Rust 更接近把资源纪律编码进静态系统；
Zig 更接近把资源纪律留给程序员、约定和工具链共同承担；
因而“资源安全”与“子结构类型系统”关系很深，但并不是同义词。

这有助于你理解：
资源安全并不只有一条语言设计路线。

10.12 会话类型：为什么子结构思想会走向通信协议

子结构类型系统另一个非常重要的延伸方向，是会话类型（session types）。

会话类型要解决的问题不是普通数据结构，而是：

两个或多个进程之间，通信必须遵守某种协议。

例如，一个简单协议可能要求：

客户端先发送请求；
服务器再返回响应；
会话结束。

在这种场景里，通道使用天然具有：

次数约束：消息不能凭空多发或少发；
顺序约束：先请求后响应，不能反过来；
线性约束：某些通信端点不能被无约束复制。

因此：

线性思想帮助保证“通道不会被随意复制或丢弃”；
有序思想帮助保证“通信顺序符合协议”。

这就是为什么会话类型和子结构逻辑之间有很深联系。

10.13 子结构类型系统的理论意义

前面的类型系统主要告诉我们：

一个值长什么样；
一个函数接受什么、返回什么；
一个表达式最终会产生什么种类的结果。

而子结构类型系统进一步告诉我们：

一个值应当怎样被使用。

如果把这一章和前几章放在一起看，可以更清楚地看到它的独特位置：

第 5 章强调“良类型程序不会卡住”；
第 8 章强调“更具体的类型如何安全替代更一般的类型”；
第 9 章强调“类型信息如何自动恢复”；
而本章强调：即使值的形状完全正确，使用方式本身也可能需要被类型系统约束。

这是一个非常重要的观念转变。

普通类型系统更关注“形状”

例如：

Bool
Nat
A × B
A → B

这些主要描述的是值的结构和计算接口。

子结构类型系统进一步关注“使用纪律”

例如：

这个值能不能复制？
能不能不用？
必须用几次？
必须按什么顺序用？

这说明类型系统的表达能力不止于“描述数据形状”，还可以用于：

控制资源；
表达协议；
限制别名；
约束副作用。

从这个角度看，子结构类型系统让“类型”从单纯的数据分类工具，扩展成了：

程序行为约束工具。

10.14 本章小结

这一章最重要的收获有四点。

1. 常规类型系统其实默认允许结构规则

我们平时习以为常的环境使用方式，实际上依赖于：

交换
弱化
收缩

这些规则之所以“看不见”，只是因为它们太常见了。

2. 子结构类型系统通过禁止部分结构规则来控制资源

禁止收缩 → 不允许复制
禁止弱化 → 不允许丢弃
禁止交换 → 不允许任意改顺序

于是类型系统开始能表达资源纪律。

3. 线性、仿射、相关、有序是不同强度的系统

仿射：至多一次
相关：至少一次
线性：恰好一次
有序：恰好一次且按顺序

其中最核心、最值得牢记的是：

线性 = 不可丢弃 + 不可复制
仿射 = 可丢弃 + 不可复制

4. 现实语言和协议系统都能从这里找到理论影子

Rust 的所有权系统与仿射 / 线性直觉密切相关；
会话类型与顺序敏感资源控制密切相关；
资源安全的语言设计不只有一种实现路径。

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

子结构类型系统把“类型描述值的形状”进一步推进为“类型约束值的使用纪律”。

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

结构规则如何进入类型判断系统；
为什么线性系统需要环境分裂；
为什么资源安全问题会自然引向仿射、线性、有序等不同纪律；
为什么 Rust、会话类型等实践方向能从这里找到理论影子。

本章练习

解释为什么“允许收缩”会让资源管理变得危险。
说明仿射类型和线性类型的区别，并各举一个更适合它们的资源场景。
为什么环境分裂是线性函数应用规则中的关键机制？
为什么不能简单说“Rust 就是线性类型系统”？
设想一个“先发送请求，再接收响应”的通信协议，说明为什么单纯的线性使用还不够，还需要顺序约束。

回看导航

如果你想继续沿这条线深入，比较自然的回看与延伸路径是：

回看第 5 章：重新确认类型判断 Γ ⊢ t : T 的基本骨架，再对照本章看“环境结构本身”是如何被修改的；
回看第 6 章中“引用与状态”的部分，重新理解为什么普通类型系统只描述“值的形状”还不够；
回看附录A《术语表》、附录B《符号速查表》，巩固“线性 / 仿射 / 相关 / 有序”“环境分裂”“线性函数类型”等核心概念；
再把本章与 Rust 的所有权 / 借用、以及会话类型的协议直觉放在一起理解，形成从理论到实践的整体视角。

也就是说，子结构类型系统并不是“最后补充的一章边角料”，而是把“类型不仅描述值是什么，还描述值该怎样被使用”这条主线推进到最鲜明位置的一章。

Keyboard shortcuts

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