线性类型

定义

线性类型（linear types）是一类源自 Girard 线性逻辑的子结构类型系统：线性值必须被恰好使用一次——不能被丢弃，也不能被复制。放松为「至多使用一次」则称仿射类型（affine types）。

用途

线性类型把「资源」的概念编入类型：文件句柄、锁、网络连接、内存块等一旦被消费即不可再用，忘记释放或重复释放都会成为编译错误。它也能安全地支持原地更新（in-place update），在纯函数式语言中实现可变性能。

语言实践

Rust 的所有权与移动语义本质上是仿射类型的工业化实现；Haskell 自 GHC 9.0 起提供 LinearTypes 扩展（线性箭头）；Clean 语言的唯一性类型、Idris 2 的定量类型理论、ATS 都属于这一谱系。

意义

线性类型让「不依赖垃圾回收的内存安全」成为可能，是近年系统语言设计最活跃的理论来源。