类型论

类型论是一类基于$\lambda$ 演算的形式理论的统称. 在类型论中, 所有数学对象都具有各自的类型, 每个数学对象则是它们的类型的实例 (有时也认为这些类型也是数学对象). 这与集合论不同, 因为集合论中, 所有数学对象都是集合. 类型论也被视为编程语言中类型系统的数学表述.

集合论中定义对象经常需要列出其所有元素, 类型论则鼓励使用规则来定义类型, 比如通过 “什么情况下一个表达式是某个类型的实例” 来定义类型的 “元素” (类似于生成元), 并定义类型的元素如何使用 (类似于万有性质). 利用这些规则可以定义新的类型以及实例. 常见的集合都可以视为类型, 比如自然数可以定义为 “由 0 和后继两个操作生成的类型”, 而元素的使用方式便是自然数归纳. 这样, 便绕开了 “元素” 和 “属于” 的概念. 这样的定义有如下好处:

•	Russell 悖论显然无法直接构造.
•	对计算机更友好 (比起集合论), 因为它不需要枚举无穷大的集合中的所有元素.

类型论中的许多构造都可以类比为范畴中的构造, 例如函数类型对应于内态射, 积类型对应积. 特别地, 在集合范畴中, 它们对应于映射集和 Descartes 积. 这种对应可以成为严格的理论: 范畴是类型论的模型, 称为类型论的范畴语义, 而类型论则是范畴的内语言.

类型论的另一个特点是, 命题在其中也视为类型, 类型论的各种构造也可以类比为命题逻辑 (或更高阶逻辑) 中的构造, 而命题的证明就是相应类型的实例. 也就是说, 在类型论中, 证明命题的过程就是用一系列规则, 构造此命题中的对象的过程. 这使得类型论可以作为数学的基础, 证明助理就利用了类型论的这种思想.

下表总结了一部分对应关系, 更详尽的对应请参见类型论–范畴论–逻辑学类比.

集合论	类型论	范畴论	逻辑学
集合	类型	对象	命题
单点集	单位类型	终对象	永真命题
空集	空类型	始对象	永假命题
元素	实例	从终对象出发的态射	证明

类型论的存在揭示了多个理论之间的联系, 并且让这些不同领域的研究可以相互影响. 与之相对的, 古代的 “类型论” 则特指 Russell 的工作, 见 Russell 简单类型论和 [Russell 1908].

形式化地定义类型论这一概念是非常困难的 (相关工作有 [Bauer–Haselwarter–Lumsdaine 2020], [Isaev 2016] 等), 但定义每个具体的类型论则相对容易许多, 比如简单类型 $\lambda$ 演算、Martin-Löf 类型论、同伦类型论、F 系统等.

1研究方式

在讨论一个类型论时, 可能会去定义一个具体的类型论 (比如 Martin-Löf 类型论), 或者根据一些使用例 (比如一个模型, 或者一些代码) 去假想一个类型论 (比如同伦类型论).

定义方式

定义一个具体的类型论时, 我们一般会定义它的句法和类型规则, 其中句法和一阶语言中句法类似, 描述如果给出合法语句, 而类型规则一般由推导规则的形式给出, 主要包含以下几种:

•	形成规则, 描述什么样的类型是合法的.
•	构造规则, 一般是对于某个特定类型, 去描述如何构造它的值 (实例), 这些规则类似于生成元.
•	消去规则, 一般是对于某个特定类型, 去描述如何使用它的值 (实例), 这里的 “使用” 类似于用万有性质来构造新的类型和实例.
•	计算规则, 描述同一个类型的构造规则和消去规则之间的抵消关系.
•	唯一性规则, 描述同一个类型的消去规则和构造规则之间的反向抵消关系.

在部分类型论中, 类型可能会有额外的规则, 比如立方类型论中每个类型都有转换规则.

模型

由于类型论是逻辑系统, 所以可以使用模型去解释它的语义. 在类型论的研究中, 模型和语义一般是同义词. 传统意义上的模型一般是一组真值表, 但类型论的模型一般在论域理论或者范畴论里定义, 定义方式是把类型论中所有的值和类型解释为这些理论中的数学对象, 然后再确保类型论中 “相等的值和类型” 在这些理论中也相等.

比如, 类型论的范畴模型一般把整个类型论解释为一个范畴, 其中类型或者语境被解释为范畴里的对象, 而值被解释为范畴里的态射, 参考概括范畴. 在这样的解释中, 类型论中相等的值的范畴论解释也必须是 (严格, 见: 等价原理) 相等的. 这里对相等的要求是一个非常强的要求, 因此很多性质有趣的范畴都必须要进行一些处理后能变成可以解释类型论的范畴. 这个过程可以参考 [Lumsdaine–Warren 2015]. 除此之外还有一些范畴论的研究是直接建立在很强的相等条件之下的, 比如泛等范畴.

部分类型论使用更接近集合论的方式定义模型, 比如偏等关系语义.

2分类方式

参见: 纯类型论; 相等类型

有多种视角给类型论分类, 比如:

•	类型的内蕴和外蕴: 在部分类型论中, 类型和值并不绑定, 表达式本身就是可以研究的对象, 它们的类型只是它们的属性. 这种类型论被称为外蕴的. 反之则叫内蕴的.

•	纯类型论视角: 类型和值之间的依赖关系决定类型论的种类, 常见情况有简单类型论、多态类型论、依值类型论.

•	相等类型的消去规则: 在依值类型论中, 相等类型的构造规则都是自反性, 但却有两种可能的消去规则, 一种是 J 公理, 一种是直接定义它构造规则的反向操作. 前者使得类型论是内涵的, 后者使得类型论是外延的.

•	是否存在非直谓性的宇宙. 纯类型论中的宇宙都是非直谓的, 而 Martin-Löf 类型论则是直谓的.

3参考文献

•	Valery Isaev (2016). “Algebraic Presentations of Dependent Type Theories”. arXiv: 1602.08504. (doi) (web)
•	Peter LeFanu Lumsdaine, Michael A. Warren (2015). “The Local Universes Model”. ACM Transactions on Computational Logic 16 (3), 1–31. (doi) (web)
•	Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine (2020). “A general definition of dependent type theories”. arXiv: 2009.05539. (doi) (web)
•	Bertrand Russell (1908). “Mathematical Logic as Based on the Theory of Types”. American Journal of Mathematics 30 (3), 222–262. (web)

术语翻译

类型论 • 英文 type theory • 德文 Typentheorie • 法文 théorie des types • 拉丁文 theoria typorum • 古希腊文 θεωρία τύπων

计算规则 • 英文 computation rule • 法文 règle de computation • 拉丁文 regula computationis

内蕴 • 英文 intrinsic

外蕴 • 英文 extrinsic