依赖类型和亚结构类型

依赖类型允许类型依赖于值，从而实现精确的规范；而线性类型和仿射类型等亚结构类型则控制资源的使用方式。

Definition

依赖类型是依赖于值的类型，允许在类型层面陈述和检查精确的属性；亚结构类型系统限制了变量（资源）的复制或丢弃方式，其中线性类型要求每个变量都只能使用一次。

Scope

本主题涵盖了超越传统系统的高级类型学：依赖类型，其中类型可以提及程序值，允许类型表达完整的规范并充当证明；以及亚结构类型（线性、仿射、所有权），它们限制了收缩和弱化（contraction and weakening）的结构规则，以跟踪资源使用、别名和生命周期。它与Curry-Howard对应关系和证明助手（proof assistants）相关。

Core questions

• 类型如何依赖于值来表达完整的程序规范？
• 依赖类型与构造性证明之间有何对应关系？
• 线性类型和仿射类型如何建模资源、所有权和内存安全？
• 这些丰富系统的可判定性和可用性之间存在哪些权衡？

Key theories

直觉（依赖）类型论

Martin-Löf的类型论统一了编程和构造性逻辑，使得类型即命题，程序即证明，为依赖类型语言和证明助手奠定了基础。

线性逻辑和线性类型

Girard的线性逻辑通过控制结构规则来改进经典逻辑和直觉逻辑，Wadler展示了基于它的线性类型如何安全地管理原地更新和资源使用。

亚结构系统的静态语义

Harper在一个统一的静态语义和动态语义框架内发展了亚结构及其他高级类型系统的元理论，阐明了它们的健全性和资源解释。

Clinical relevance

依赖类型为证明助手和经过验证的软件提供了支持，这些软件带有机器检查的正确性保证。亚结构类型和所有权类型是内存安全和并发安全系统语言的基础，允许在没有垃圾回收器的情况下进行安全的手动资源管理。

History

Martin-Löf的直觉类型论（1970年代-1980年代）确立了依赖类型和“命题即类型”（propositions-as-types）的观点，从而产生了Coq、Agda和Lean等证明助手。Girard在1987年提出的线性逻辑引入了资源敏感推理；Wadler的线性类型将其引入语言设计，而所有权和借用检查（borrow-checking）规范后来使亚结构思想在系统编程中成为主流。

Debates

表达力与可用性和可判定性之间的权衡

依赖类型和亚结构系统可以表达非常强的保证，但它们增加了程序员的负担，并可能使类型检查变得不可判定或繁琐，从而引发了关于多少能力值得付出代价的争论。

Key figures

• Per Martin-Löf
• Jean-Yves Girard
• Philip Wadler
• Robert Harper

Seminal works

• martinlof1984
• girard1987
• wadler1990
• harper2016

Frequently asked questions

什么是依赖类型？

依赖类型是一种其定义依赖于值的类型，例如特定长度向量的类型，这使得类型系统能够强制执行普通类型无法表达的丰富不变性。

线性类型保证了什么？

线性类型要求每个值只能使用一次，这使得编译器能够安全地允许原地更新、管理资源并防止与别名相关的错误，而无需运行时垃圾回收。