子类型

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

渐进类型理路渐进类型Gradual typing · Gradually typed lambda calculus · 渐变类型给出含函数包装的cast核心及安全性证明，并在一阶立即调用片段证明注解擦除的静态与动态渐进保证。的一致性关系回答已知信息是否冲突：Int 与未知类型一致，未知类型又与 Bool 一致，但 Int 与 Bool 不一致，因此它不具备子类型的传递性。描述注解信息多少的精度关系也不同于可替代性；其函数参数和结果都沿相同的信息遗忘方向变化。

结构记录中，若只读字段采用宽度子类型，则 {x:Int,y:Int}<:{x:Int}：需要x的代码可以忽略额外的y。若还要求修改一个字段后在结果类型中保留其余字段，可用行多态理路行多态Row polymorphism · Row types以开放行变量保留记录的未知字段，并用标签无序相等和lacks约束维持唯一标签。让输入输出共享同一个未知行；单独的闭合 {x:Int}→{x:Int}签名不会记录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$，复杂系统还需处理交、并、递归类型与有界量化。

在只有基础类型、Top、箭头和只读记录的可观察递归图中，循环子类型判定理路递归结构子类型判定Recursive structural subtyping · Equi-recursive subtyping algorithm在有限递归类型图上展开有方向的替代义务，以只读记录宽度和函数域逆变生成闭合证书，并返回带方向的有限失败路径。可用有限有序节点对终止：方法参数生成反向义务，结果和字段保持原方向。重复对只登记本次待检查假设，整份义务封闭后才发布成功；无守卫传递规则不能直接加入结构最大不动点，否则错误判断也能用无限自引获得接受。

它与参数多态理路参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。是不同复用机制：前者允许较具体值向上转换，后者要求同一代码对所有类型参数统一工作。类型判断理路类型判断Typing judgment由类型规则推导的上下文判断，记录项在给定变量假设下具有的静态类型。通过 subsumption 接纳子类型，而类型安全理路进展与保持定理Progress and preservation · Type safety对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。约束每条子类型规则必须保持运行时行为。