次结构类型系统

次结构类型系统是一个类似于次结构逻辑的类型系统家族，其中一个或多个结构规则不存在或只在受控情况下允许存在。这类系统通过跟踪发生的状态变化和防止无效状态，对于约束对系统资源（如文件、锁和内存）的访问非常有用。

通过抛弃一些交换、弱化和收缩的结构规则，出现了一些类型系统。有序类型系统（抛弃交换、弱化和收缩）。每个变量都按照它被引入的顺序精确使用一次。线性类型系统（允许交换，但不允许削弱或收缩）。Affine类型系统（允许交换和减弱，但不允许收缩）。每个变量最多使用一次。相关类型系统（允许交换和收缩，但不能削弱）。每个变量至少被使用一次。普通类型系统（允许交换、削弱和收缩）。对仿生类型系统的解释，如果改写为"一个变量的每一次出现都最多使用一次"，就能得到xxx的理解。

有序类型对应于非交换逻辑，其中交换、收缩和弱化被抛弃。这可以用来模拟基于堆栈的内存分配（与线性类型相比，后者可以用来模拟基于堆的内存分配）。如果没有交换属性，一个对象只能在建模的堆栈顶部被使用，之后它就会被弹出，导致每个变量按其被引入的顺序被精确使用一次。

线性类型对应于线性逻辑，确保对象被精确使用一次。这允许系统在使用完一个对象后安全地去分配它，或者设计软件接口，保证资源一旦被关闭或过渡到不同的状态就不能被使用。Clean编程语言利用xxx性类型（线性类型的一个变种）来帮助支持并发、输入/输出和数组的就地更新。线性类型系统允许引用，但不允许别名。为了执行这一点，一个引用在出现在赋值的右侧后就会超出范围，从而确保对任何对象的引用一次只存在一个。请注意，将一个引用作为参数传递给一个函数是一种赋值形式，因为函数参数将在函数中被赋值，因此对引用的这种使用也会导致它超出范围。线性类型系统类似于C++的unique_ptr类，它的行为类似于指针，但在赋值中只能被移动（即不能被复制）。尽管线性约束是在编译时检查的，但解引用一个无效的unique_ptr会在运行时导致未定义的行为。

同样，Rust编程语言通过使用lint注解对线性类型有部分支持，但与C++不同的是，从变量中移出的变量不能再次使用。单一引用的特性使得线性类型系统适合作为量子计算的编程语言，因为它反映了量子态的无克隆定理。从范畴理论的角度看，不克隆是一个声明，即没有对角线放函数可以复制状态；同样，从组合逻辑的角度看，没有K组合器可以破坏状态。从lambdacalculus的角度来看，一个变量x在一个术语中可以精确地出现一次。线性类型系统是封闭的对称单数范畴的内部语言，就像简单类型的λ微积分是笛卡尔封闭范畴的语言一样。更确切地说，我们可以在线性类型系统的范畴和封闭对称单项类的范畴之间构造漏子。

仿生类型是线性类型的一个版本，允许丢弃（即不使用）一个资源，对应于仿生逻辑。一个仿生资源最多可以使用一次，而一个线性资源必须正好使用一次。

相关类型对应于相关逻辑，它允许交换和收缩，但不允许削弱，这意味着每个变量至少被使用一次。