形式陈述

子类型关系 $S<:T$$S<:T$ 表示任何 $S$$S$ 类型值都可在期望 $T$$T$ 的位置安全使用。它通常至少是自反、传递的预序，并通过 subsumption 规则进入类型系统：

$$ \frac{\Gamma\vdash t:S\qquad S<:T}{\Gamma\vdash t:T}. $$$$\frac{\mathrm{\Gamma }⊢t:SS<:T}{\mathrm{\Gamma }⊢t:T}.$$

互为子类型不必是语法相等；按 $S\equiv T\iff S<:T\land T<:S$$S\equiv T⟺S<:T\wedge T<:S$ 取商后才得到反对称的偏序。函数类型满足参数逆变、结果协变：若 $T_1<:S_1$$T_1<:S_1$ 且 $S_2<:T_2$$S_2<:T_2$，则 $S_1\to S_2<:T_1\to T_2$$S_1\to S_2<:T_1\to T_2$。

直觉

子类型不是“名字相似”，而是一项替换承诺：较具体的值必须支持较一般上下文所依赖的全部行为。

例子与边界

只读记录常有宽度子类型：含字段 {x:Int,y:Int} 的值可用于只要求 {x:Int} 的位置。函数参数方向相反，因为接受更一般输入的函数才能替代只要求较窄输入的函数。类继承可能产生子类型，但若违反行为契约，名义继承并不自动保证语义可替换性。可变引用通常需要不变性，否则读写组合会破坏类型安全。

推论与应用

子类型支持接口抽象、对象系统、记录演化和渐进类型。算法层面需决定关系并插入 coercion；元理论上要证明 subsumption 与动态语义共同保持类型安全。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 15–18, subtyping, records, and variants。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Chs. 21–24, subtyping and variance。