子结构类型系统

形式陈述 ​

普通类型系统常把上下文当作可任意增补、复制或重排的假设集合。子结构类型系统显式选择哪些结构规则可用。对判断 $\mathrm{\Gamma }⊢e:B$，三条核心规则可表示为：

$$\frac{\mathrm{\Gamma }⊢e:B}{\mathrm{\Gamma },x:A⊢e:B}(\mathsf{weakening}),$$$$\frac{\mathrm{\Gamma },x:A,y:A⊢e:B}{\mathrm{\Gamma },z:A⊢e[z/x,z/y]:B}(\mathsf{contraction}),$$$$\frac{\mathrm{\Gamma },x:A,y:C,\mathrm{\Delta }⊢e:B}{\mathrm{\Gamma },y:C,x:A,\mathrm{\Delta }⊢e:B}(\mathsf{exchange}).$$

弱化允许加入未使用的假设，因而允许丢弃资源；收缩把两个同型假设合成一个可重复使用的假设，因而允许复制；交换允许改变使用次序。在普通类型判断公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。中，这些能力往往由上下文表示隐含，子结构系统则把它们是否可采纳变成类型理论的一部分。

线性函数应用展示了资源如何被分配，而不是同时把整份上下文交给两个前提：

$$\frac{\mathrm{\Gamma }⊢e_1:A⊸B\mathrm{\Delta }⊢e_2:A}{\mathrm{\Gamma }\uplus \mathrm{\Delta }⊢e_1{e}_2:B}.$$

$\mathrm{\Gamma }\uplus \mathrm{\Delta }$ 要求两侧线性资源不重叠，因此同一变量不能未经许可同时供函数项和参数项使用。这是声明式上下文分割规则；类型检查器可以搜索分割，也可以用使用量标注或双向检查直接计算分配，但算法不能悄悄恢复被逻辑禁止的复制。

常见分类由允许的结构规则定位：线性系统通常禁止弱化和收缩但允许交换，资源必须恰好使用一次；仿射系统允许弱化而禁止收缩，资源至多使用一次；相关系统允许收缩而禁止弱化，假设不能完全闲置；有序或非交换系统还限制 exchange，使使用顺序有意义。不同文献会把这些限制与模态、多个上下文或其他规则组合，名称应以具体演算为准。

直觉 ​

若把上下文条目只看成事实，同一个事实多用几次或不用似乎无关紧要；若条目代表会被消费的能力，复制和丢弃就会改变程序含义。一次性通信端点、唯一写权限或必须履行的协议步骤都更像票据：把票复印两份不能合法获得两次服务，把它遗忘也可能留下未完成义务。

子结构类型没有为资源预先指定某种物理形态。它只是控制证明和程序中假设如何流动；文件句柄、内存所有权、会话端点或隐私预算能否由此安全建模，还取决于相应原语的运行语义。

例子与边界 ​

设 send : Msg ⊗ Chan S ⊸ Chan S' 消费处于协议状态 $S$ 的端点，并返回状态推进到 $S^{\prime }$ 的新端点。调用后继续使用旧端点会要求收缩同一线性变量，类型规则拒绝它；完全忘记返回的新端点则要求弱化，也会在线性系统中被拒绝。若接口采用仿射端点，提前放弃可被允许，但复制后发送两次仍不合法。

闭包捕获不会绕过资源规则。若函数体捕获一个线性端点，那么生成的闭包本身必须按线性方式使用；否则复制闭包就等于间接复制端点。分支也需要专门的资源规则：同一资源可以出现在互斥的两个分支中，并不等于一次运行会消费两次，因此不能把类型层纪律粗暴实现为纯文本变量出现次数统计。

静态“使用一次”也不等于运行时只分配一块内存或机器指令只访问一次。递归、控制流与优化会改变动态执行次数；可靠结论必须由类型规则和运行语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。之间的保持性质给出。子结构类型能排除未经授权的别名或丢弃，却不会自动消除所有内存泄漏、死锁或数据竞争。

推论与应用 ​

在Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，结构规则的限制连接程序资源与命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。的子结构变体，特别是线性逻辑。普通可复制值可通过 unrestricted 模态或与线性上下文分离的持久上下文重新获得弱化和收缩，不必把整数常量、只读配置等所有值都强制当作一次性资源。

子结构系统为线性与仿射类型、所有权与借用、会话类型和资源感知验证提供共同上位框架。具体语言通常选择其中一部分纪律，并增加生命周期、区域或协议状态；这些机制建立在结构规则之上，但不能反过来把“子结构类型”缩写成某一种语言的所有权检查器。

参考资料

• Jean-Yves Girard, “Linear Logic,” Theoretical Computer Science 50, 1987。
• David Walker, “Substructural Type Systems,” in Advanced Topics in Types and Programming Languages, MIT Press, 2005。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，resource-sensitive typing。