空类型

空类型是空集在类型论中的类比, 就是没有实例的类型. 它在简单类型论和依值类型论里都可以定义, 且定义是一样的.

1类型规则

空类型记作 $\varnothing$.

构造规则

正如空集没有元素, 空类型没有构造规则.

消去规则

对应逻辑学中的爆炸律.

$$\frac{\Gamma ⊢A\mathrm{type}}{\Gamma ⊢{\mathrm{rec}}_{\varnothing }:\varnothing \to A}$$

因为空类型没有构造规则, 所以不需要计算规则.

2应用

空类型可以用于定义 “某类型没有实例” 这个命题:

定义 2.1. 对于类型 $A$, 它没有实例是指如下类型存在实例$$\neg A:=A\to \varnothing$$

之所以说这是命题是因为它确实是命题宇宙意义上的命题:

引理 2.2. 对于类型 $A$, 以下命题成立: $$\mathrm{isProp}(\neg A)$$

3变种

子类型

底类型是子类型意义上的空类型, 它的定义和空类型一样: 没有实例的类型. 但在讨论子类型的类型论中, 空类型显然是子类型关系构成的格中的最小元素, 因此又称之为底类型, 一般记作 $\perp$.

$\lambda$ 编码

参见: lambda 编码

在 F 系统中可以编码空类型, 直接将空类型定义为如下类型即可:

$$\varnothing :=\forall A.A$$

很显然可以构造出该类型到任何其它类型的函数.

依值类型论中用 $\Pi$ 类型和宇宙代替上述类型:

$$\varnothing :={\Pi }_{A:\mathcal{U}}A$$

4应用

•	一致性
•	编码-解码法

术语翻译

空类型 • 英文 empty type • 德文 leerer Typ • 法文 type vide • 拉丁文 typus vacuus • 日文 空型

底类型 • 英文 bottom type