线性类型与仿射类型

形式陈述 ​

线性类型是子结构类型系统公理库子结构类型系统Substructural type system · Resource-sensitive type system通过限制弱化、收缩或交换等上下文结构规则，静态约束假设与程序资源的使用方式。中同时禁止 weakening 与 contraction 的分支：线性假设既不能丢弃，也不能复制，因而必须恰好使用一次。仿射类型允许 weakening 而仍禁止 contraction，假设可以不用，但至多使用一次。“恰好一次”与“至多一次”的差别正是二者的定义边界。

一种最小形式使用双上下文判断

$$\mathrm{\Gamma };\mathrm{\Delta }⊢e:A,$$

其中持久上下文 $\mathrm{\Gamma }$ 中的变量可弱化、收缩，线性上下文 $\mathrm{\Delta }$ 中的变量必须按所选纪律消费。线性函数公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。的引入与应用规则可写为

$$\frac{\mathrm{\Gamma };\mathrm{\Delta },x:A⊢e:B}{\mathrm{\Gamma };\mathrm{\Delta }⊢\lambda x.e:A⊸B},$$$$\frac{\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:A⊸B\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢e_2:A}{\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢e_1{e}_2:B}.$$

不相交分割 ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2$ 保证一个线性变量只进入一个前提。仿射系统使用同样的禁止重叠规则，但允许从结论上下文丢弃未分配变量；线性系统若无显式消费操作则不允许这样做。

线性积通常写成 tensor $A\otimes B$，构造一对时同样分割资源：

$$\frac{\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:A\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢e_2:B}{\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢(e_1,e_2):A\otimes B}.$$

它与普通笛卡尔积公理库积类型Product type其值由两个分量组成并支持投影的类型。不能无条件混用：普通投影取一项会丢弃另一项，而拆解 tensor 必须让两个分量都进入后续线性上下文，或由仿射规则明确允许丢弃。

可复制值可通过持久上下文或指数模态 $!A$ 引入。一组最小规则是

$$\frac{\mathrm{\Gamma };\varnothing ⊢v:A}{\mathrm{\Gamma };\varnothing ⊢!v:!A},\frac{\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:!A\mathrm{\Gamma },x:A;{\mathrm{\Delta }}_2⊢e_2:B}{\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢\mathsf{let}!x=e_1\mathsf{in}{e}_2:B}.$$

promotion 要求没有未消费线性资源，防止把线性捕获藏进可复制值；消去后 $x$ 进入 $\mathrm{\Gamma }$，才可复制或忽略。不同语言也会采用 usage grades、borrowed context 或类型类表达可复制性，但都必须说明哪类变量恢复了结构规则。

直觉 ​

线性值像必须交接的一次性权利：拿到它就必须沿唯一一条路径使用并产生下一阶段资源。仿射值更像不可复印但可以作废的票据。持久值则像一段公开信息，可以反复读取；把三者混在一个普通上下文中，会让复制和丢弃重新变得不可见。

类型检查器实现的上下文分割是算法问题，声明式规则只规定存在一个合法分配。实现可回溯搜索、给每个子项计算使用集合，或用双向规则传播需求；无论采用哪种算法，都必须证明接受的程序对应一棵合法线性/仿射推导。

例子与边界 ​

一次性会话端点可让 send 消费 $\mathsf{Chan}(S)$ 并返回 $\mathsf{Chan}(S^{\prime })$。发送后继续使用旧端点需要复制同一线性变量，因而被拒绝；忘记新端点也在线性系统中不合法。新的端点值把协议状态推进显式化，而不是在原值背后偷偷改变类型。

仿射文件句柄允许程序在错误路径提前放弃句柄，却不允许复制句柄后关闭两次。若资源必须可靠关闭，单纯仿射“可丢弃”仍太弱，还需析构、作用域或 finally 规则保证释放；因此仿射类型不会自动消除泄漏。

整数常量和只读配置不应因为语言支持线性资源就只能使用一次。它们可直接放在 $\mathrm{\Gamma }$，或具有 $!\mathsf{Int}$ 一类 unrestricted 类型。若闭包捕获 $\mathrm{\Delta }$ 中的端点，创建闭包会消费该绑定，所得闭包也必须线性使用；否则复制闭包就会间接复制端点。

推论与应用 ​

线性和仿射纪律可约束唯一引用、会话协议、资源释放和并发能力，但类型层的使用次数不等于运行时只访问一次或只分配一块内存。分支、递归与优化会改变动态步骤；可靠结论来自类型保持：求值不能复制或遗失被静态标记为线性的资源所有权。

所有权与借用系统受这些思想启发，却还要加入别名、生命周期、重借用和内部可变性规则；它不是线性类型的同义词。线性类型也不会仅凭禁止 contraction 自动消除数据竞争、死锁或所有内存泄漏。

参考资料

• Jean-Yves Girard, “Linear Logic,” Theoretical Computer Science 50, 1987。
• Philip Wadler, “Linear Types Can Change the World!” in Programming Concepts and Methods, 1990。
• David Walker, “Substructural Type Systems,” in Advanced Topics in Types and Programming Languages, MIT Press, 2005。