子类型关系

安全替换原则

在TAT中，一个变量x的类型若为{a: Num}，你能够对它做的唯一特殊的操作，就是x.a。 x.a这个操作预期得到一个Num类型的变量而不会发生运行时错误。因此，若在一个期望类型为{a: Num}的地方，传入一个要求更高的值{a: 1, b: 2}，也完全符合"得到一个Num类型而不会发生运行时错误"的预期。

那么，{a:1, b:2}也就成为了一个合法的{a: Num}。

我们把这种对替换的直觉，归纳成为子类型的安全替换原则。如下：

若我们可以将任何 $T$ 类型的值替换为 $S$ 类型的值而安全使用，那么我们称 $S$ 是 $T$ 的子类型，记做 $S <: T$ 。

这里说的安全使用，可以理解成不产生运行时错误。

这里用的子类型关系记号<:，其实也是在暗示这种关系是一种特殊的"大小关系"（用数学一点的说法来说，是一种序关系）。你可以将它类比为集合的 $\subseteq$ 关系，或是数字的 $\leq$ 关系。

形式化子类型关系

我们在TAT的类型系统中，扩展一下定型规则，使其引入子类型。

{ \Gamma \vdash t: S \quad S<: T \over \Gamma \vdash t : T } \tag{T-Sub}

这个规则的意思是说，若 $S$ 是 $T$ 的子类型，那么 $S$ 类型的项也是 $T$ 类型的项。

类型 $S$ 和类型 $T$ 的关系如下：

$S$ 是 $T$ 的子类型。
$S$ 比 $T$ 信息更丰富、要求更高。

例如，直觉上来看，类型 $\{a:\text{Num}, b: \text{Num}\}$ 比类型 $\{a:\text{Num}\}$ 更严格、实例数量更少、要求更高。

若将类型看成一个集合，类型 $\{a:\text{Num}, b: \text{Num}\}$ 是类型 $\{a:\text{Num}\}$ 的真子集。前者的所有元素都是后者的元素。