子类型

子类型不是“结构看起来像”或“类继承了谁”，而是上下文中的可替代性承诺。函数参数逆变最容易反直觉：一个能处理所有动物的函数当然能放到只会收到猫的位置，而只处理猫的函数不能冒充能处理所有动物的函数。结果则相反，返回更具体的猫可安全当作返回动物。定义中的方向由谁提供、谁消费数据决定，而不是由语法箭头机械决定。

结构记录中，若只读字段采用宽度子类型，则 {x:Int,y:Int}<:{x:Int}：需要 x 的代码可以忽略额外的 y。函数 Animal→Cat 可作为 Cat→Animal 使用，因为它接受范围更广、返回结果更具体。

边界是可变引用。若假设 Ref Cat <: Ref Animal，代码可通过 Ref Animal 写入一只狗，原持有者随后从 Ref Cat 读出狗，类型承诺被破坏；因此可读写引用通常不变。名义继承也不自动等于行为子类型，违反方法契约的子类不能仅凭语法继承获得可靠替代性。

子类型支撑面向对象接口、记录扩展、数值层次和 API 演化。所有权与借用公理库所有权与借用Ownership and borrowing · Ownership type system · Borrow checking以所有者、移动、共享或独占借用及生命周期约束静态组织资源责任与别名访问。还会把生命周期包含解释成引用可缩短使用区间的 region subtyping；独占 reborrow 与可变引用的 variance 另有别名约束，不能从普通协变机械推出。算法类型检查需要决定 $S<:T$，复杂系统还需处理交、并、递归类型与有界量化。

它与参数多态公理库参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。是不同复用机制：前者允许较具体值向上转换，后者要求同一代码对所有类型参数统一工作。类型判断公理库类型判断Typing judgment由类型规则推导的上下文判断，记录项在给定变量假设下具有的静态类型。通过 subsumption 接纳子类型，而类型安全公理库进展与保持定理Progress and preservation · Type safety在固定动态语义下，良类型闭项可继续或已是结果，且每一步都保持其类型。约束每条子类型规则必须保持运行时行为。