子类型

在类型论中, 子类型是集合之间子集概念的类比.

集合论中的子集有两种观点, 集合 $A$ 的子集 $B$ 一方面可以视作 $A$ 的幂集中的元素 $B\in \mathcal{P}(A)$, 另一方面可以视作集合 $B$ 到集合 $A$ 的嵌入 $i:B\hookrightarrow A$. 与之相对应, 类型论也有两种子类型的概念, 被称为质料子类型和结构子类型.

1定义

质料子类型

定义 1.1. 记 $\Omega \equiv \mathrm{Prop}$ 为命题宇宙 (或将其视作子对象分类子的真值对象), 定义 $A$ 的幂类型为从 $A$ 到 $\Omega$ 的函数类型:

$$\mathcal{P}(A):\equiv (A\to \Omega )$$

定义 1.2. 定义 $A$ 的质料子类型为其幂类型中的元素 $B:\mathcal{P}(A)$.

定义 1.3. 定义 $A$ 中元素 $x:A$ 和质料子类型 $B:\mathcal{P}(A)$ 之间的局部属于关系 $x{\in }_{A}B$ 为: $$x{\in }_{A}B:\equiv B(x)$$

结构子类型

定义 1.4. 对于函数 $f:B\to A$, 我们称 $f$ 为嵌入, 当且仅当对任意 $x,y:B$, 函数$${\mathrm{ap}}_f:(x{=}_{B}y)\to (f(x){=}_{A}f(y))$$为等价.

定义 1.5. $A$ 的结构子类型是二元组 $(B,i_B)$, 其中 $B$ 是类型, $i_B$ 是 $B$ 到 $A$ 的嵌入 $i_B:B\hookrightarrow A$.

质料子类型与结构子类型的比较

质料子类型和结构子类型之间有一一对应的关系.

给定质料子类型 $P_B:\mathcal{P}(A)$, 其对应的结构子类型可以表达为:$$\begin{gathered} i_B:B\equiv \sum _{x:A}{P}_B(x)\hookrightarrow A \\ (x,y)\mapsto x \end{gathered}$$

反之, 给定结构子类型 $i_B:B\hookrightarrow A$, 相应质料子类型可以表达为:

$$P_B=\left(\lambda x:A.\sum _{y:B}{i}_B(y){=}_{A}x\right):\mathcal{P}(A)$$

另外, 定义函数 $\lambda x.1:1\to \Omega$, 那么可将其视作一种子类型分类子. 具体来说, 质料子类型 $P_B:\mathcal{P}(A)$ 与其对应的结构子类型 $(B,i_B:B\hookrightarrow A)$ 可构成如下的拉回图表:

$$B1A\Omega i_B┌\lambda x.1P_B$$

外延子类型

警告. 本定义不被主流数学界所采用.

定义 1.6. 若对于任意 $u$ 满足 $\Gamma ⊢u:A$, 都有 $\Gamma ⊢u:B$, 那么 $A$ 是 $B$ 的子类型, 记作 $A:<B$.

该定义可以写作类型规则: $$\frac{\Gamma ⊢A:<B\Gamma ⊢u:A}{\Gamma ⊢u:B}$$该性质又叫 Liskov 替换原则.

这种子类型的定义存在明显的问题. 若 $A:<B$, 那么 $A$ 的实例就是 $B$ 的实例, 这使得一个值可以对应多个不等价的类型, 违背了类型论中的内涵性思想.

术语翻译

子类型 • 英文 subtype

质料子类型 • 英文 material subtype

结构子类型 • 英文 structural subtype

局部属于关系 • 英文 local membership relation

Liskov 替换原则 • 英文 Liskov substitution principle (LSP)