子类型

在类型论中, 子类型指一种类型上的二元关系, 类似集合之间的子集关系, 记作 $A:<B$, 其中 $A$ 是 $B$ 的子类型.

1定义

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

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

这类似类型等价, 但子类型并不是一个对称关系.

与嵌入的关系

正如 “$A\subseteq B$” 和 “存在一个单射 $p:A\to B$” 的区别一样, 子类型和 “两类型存在单射” 也不应该看作等价的概念, 即使两者高度相似, 且后者常常被用于模拟前者.

若 $A:<B$, 那么 $A$ 的实例就是 $B$ 的实例, 这使得一个值可以对应多个不等价的类型, 违背了类型论中很核心的思想.

参数化类型

定义 1.2. 考虑类型上的操作 $F$:

$$\frac{\Gamma ⊢A}{\Gamma ⊢F(A)}$$

若满足

$$\frac{\Gamma ⊢A:<B}{\Gamma ⊢F(A):<F(B)}$$

则称 $F$ 是协变的, 若

$$\frac{\Gamma ⊢A:<B}{\Gamma ⊢F(B):<F(A)}$$

则称 $F$ 是反变的.

这里的协变、逆变和函子中类似的概念使用相同的术语.

2后果

相比起用单射模拟子类型, 直接引入子类型会对类型论带来灾难性破坏, 它分离了语境中的类型和语境中变量实际的类型, 从而对类型论中最重要的替换操作的性质带来剧变.

具体来说, 考虑如下相继式:

$$x:A,y:B⊢f(x,y):C$$

若类型论没有子类型 (或者说有平凡的子类型, 即仅允许子类型为自反关系), 那么此时可以假设变量 $x$ 的类型就一定是 $A$. 但若类型论有非平凡的子类型, 那么 $x$ 的类型只能被假设为某 $A$ 的子类型, 若我们严格需要一个类型为 $A$ 的实例 (而不是 $A$ 的子类型), 就不能使用 $x$, 或者在语境里引入额外的限制方法, 这又会大大降低子类型带来的灵活性, 得不偿失.

3相关概念

•	单位类型在子类型中的对应物叫顶类型, 所有类型都是它的子类型.
•	空类型在子类型中的对应物叫底类型, 它是所有类型的子类型.

术语翻译

子类型 • 英文 subtype

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