依值类型论

依值类型论是一种类型的定义可以依赖于值的类型论, 也就是说类型由如下相继式引入:$$\Gamma ⊢A\mathrm{type}$$在现代提到依值类型论时, 一般会默认这个类型论也是多态类型论. 因此, 与依值类型论相对的类型论也就被默认为简单类型 $\lambda$ 演算了. 依值类型论和简单类型论的区别可以简单的理解为: 后者中语法正确的类型都是合法的类型, 但前者构造类型时需要在一个语境中讨论. 在依值类型论中, 语境的概念比起类型本身要重要得多, 因为类型和值都需要在语境中讨论.

就像类型论一样, 依值类型论的概念本身也很难准确定义, 但 Martin-Löf 类型论 (包括在此之上建立的类型论, 比如同伦类型论)、构造演算等属于依值类型论的具体类型论则可以相对容易地形式化定义, 因为它们有具体的语法.

依值类型论一般包含 $\Sigma$ 类型、$\Pi$ 类型和宇宙. 依值类型论和类似的理论有如下对应关系:

数理逻辑	依值类型论	范畴论
语境	语境	对象
命题	类型	俯范畴里的对象
命题宇宙	命题宇宙	子对象分类子
全称量词	$\Pi$ 类型	依值积
存在量词	$\Sigma$ 类型	依值和

1基本思想

首先, 依值类型论中的类型定义是由如下形式的相继式写出的, 其中 $\Gamma$ 是一个语境, 而 $A$ 是一个语法合法的类型:

$$\Gamma ⊢A\mathrm{type}$$

语境

定义 1.1. 依值类型论中的语境 $\Gamma$ 由如下两条规则归纳生成:

•	空语境 (即什么假设也不包含的语境) 是合法的语境.

•	考虑合法的语境 $\Gamma$, 如果 $\Gamma ⊢A\mathrm{type}$, 那么 $\Gamma ,A$ 也是一个合法的语境, 而这个通过拼接语境和类型得到新的语境的过程叫做语境延伸.

在依值类型论中, 类型、值、语境这三个概念 (有时还会加上宇宙, 一共四个概念) 的定义是互递归的. 这给依值类型论带来了强大的表达力, 但也使得定义和证明依值类型论的性质变得异常困难.

注 1.2. 在考虑变量名的情况下, 语境会写成 $\Gamma ,x:A$ 这样的形式, 方便在 $⊢$ 右边引用变量 $x$. 但是这里这个变量名没有被用到, 而且我们希望尽可能在语法上体现 $\alpha$ 等价性, 所以就省略了变量名.

替换操作

在简单类型论的替换操作基础之上, 依值类型论引入了类型上的替换操作, 且需要满足如下原则:

•	任何替换 $\sigma :\Gamma \to \Delta$ 都需要能和类型 $\Delta ⊢A\mathrm{type}$ 操作得到 $\Gamma ⊢A\sigma \mathrm{type}$.

•	任何替换 $\sigma :\Gamma \to \Delta$ 都需要能和值 $\Delta ⊢u:A$ 操作得到 $\Gamma ⊢u\sigma :A\sigma$.

这个过程十分类似纤维范畴中诱导函子的过程, 这也引来了范畴语义的研究.

处理宇宙

参见: 宇宙 (类型论)

由 Russell 悖论可知不能存在包含自己的集合, 类似的悖论在依值类型论中也存在, 即 Girard 悖论, 内容就是不能存在以自己为类型的类型. 因为在依值类型论中, 类型也是一种值, 所以有宇宙 (记作 $\mathcal{U}$) 来代表类型的类型, 比如 $\mathbb{N}:\mathcal{U}$、$\mathbb{N}\to \mathbb{N}:\mathcal{U}$, 但宇宙的类型就不能是自己. 对于宇宙的类型, 有两类处理方式:

•	使用 Tarski 宇宙, 即规定 $A:\mathcal{U}$ 和 $A\mathrm{type}$ 是两种不同的相继式, 然后再说宇宙是一种类型, 但宇宙作为一个值却没有类型.

•	使用宇宙层级, 即给宇宙带上一个自然数下标 ${\mathcal{U}}_i$, 然后说一般的类型的类型是 ${\mathcal{U}}_0$, 但 ${\mathcal{U}}_0:{\mathcal{U}}_1$, 以此类推.

这两种处理方式并不冲突, 在讨论语义的时候一般是两者同时使用.

2语义研究

依值类型论有丰富的语义研究, 在范畴论、集合论、论域理论中都能构造出模型.

范畴语义

可以在一个概括范畴里解释依值类型论. 总体思想是在一个语境为对象、替换操作为态射的范畴 $\mathsf{Ctx}$ 中构造如下集合, 并赋予一些结构:

•	对于 $\Gamma \in \mathrm{Ob}\mathsf{Ctx}$, 所有该语境下的类型构成的集合 $Ty(\Gamma )$.

•	对于 $\Gamma \in \mathrm{Ob}\mathsf{Ctx}$ 和 $A\in Ty(\Gamma )$, 所有该类型的实例构成的集合 $Tm(\Gamma ,A)$.

定义这些集合、并证明这些类型支持 替换操作 中提到的操作, 便解释了依值类型论.

术语翻译

依值类型论 • 英文 dependent type theory • 法文 théorie des types dépendants • 拉丁文 theoria typorum dependentium • 古希腊文 θεωρία τύτων ἐξαρτωμένων

替换 • 英文 substitution • 法文 substitution (f) • 拉丁文 substitutio (f)