名称: 子类型验证器
描述: ‘验证类型系统中的子类型关系。使用场景：(1) 实现类型系统，(2) 证明类型安全，(3) 检查多态性。’
版本: 1.0.0
标签:
- 类型系统
- 子类型
- 继承
- 多态性
难度: 中级
语言:
- python
- ocaml
依赖:
- 类型检查器生成器
子类型验证器
验证类型系统中的子类型关系。
使用场景
- 实现类型系统
- 证明类型安全
- 检查多态代码
- 形式验证
此技能的作用
- 定义子类型规则 - 结构/名义子类型
- 检查关系 - 验证 τ₁ <: τ₂
- 处理记录 - 宽度/深度子类型
- 证明传递性 - 组合子类型证明
如何使用
- 定义类型构造函数（
TInt, TFun, TRecord 等）
- 实现基本关系规则（自反性、传递性）
- 添加结构规则（记录宽度/深度、函数方差）
- 使用正面和负面示例进行验证
使用示例
checker = SubtypingChecker()
# Int <: Int
assert checker.is_subtype(TInt(), TInt()) == True
# {x:Int, y:Int} <: {x:Int} (宽度)
sub = TRecord({'x': TInt(), 'y': TInt()})
super_type = TRecord({'x': TInt()})
assert checker.is_subtype(sub, super_type) == True
# {x:Int} <: {x:Int, y:Int} (不 - 缺少字段)
assert checker.is_subtype(super_type, sub) == False
# 函数反变性
# (Int → Bool) <: (Bool → Bool)
# 检查: Bool <: Int (假), Bool <: Bool (真)
f1 = TFun(TInt(), TBool())
f2 = TFun(TBool(), TBool())
assert checker.is_subtype(f1, f2) == False
# (Bool → Bool) <: (Int → Bool)
# 检查: Int <: Bool (假), Bool <: Bool (真)
assert checker.is_subtype(f2, f1) == False
# 正确的反变性示例:
# (Animal -> Cat) <: (Cat -> Animal)
# 域检查: Cat <: Animal (真，反转)
# 共域检查: Cat <: Animal (真，协变)
f_sub = TFun(TAnimal(), TCat())
f_sup = TFun(TCat(), TAnimal())
assert checker.is_subtype(f_sub, f_sup) == True
关键概念
| 概念 |
描述 |
| 宽度子类型 |
允许更多字段 |
| 深度子类型 |
兼容的字段类型 |
| 反变性 |
函数域反转 |
| 协变性 |
与层次结构同方向 |
| 双变性 |
通常对函数参数不健全；除非受限，避免使用 |
经典参考文献
| 参考 |
重要性 |
| Cardelli, “A Theory of Objects” |
面向对象子类型的正式处理 |
| Abadi & Cardelli, “A Theory of Primitive Objects” |
方法类型和子类型 |
| Pierce, “Types and Programming Languages”, Ch. 15-16 |
全面的子类型覆盖 |
| Gay & Hole, “Subtyping for Session Types” |
通信类型的子类型 |
| Eifrig et al., “Sound Polymorphic Type Inference for Objects” |
面向对象类型推断 |
提示
- 从简单的结构子类型开始
- 需要时添加名义子类型
- 小心处理递归
- 与实现一起证明健全性
相关技能
type-checker-generator - 类型检查type-inference-engine - 类型推断hoare-logic-verifier - 健全性证明
研究工具与成果
编译器中的子类型：
| 工具 |
学习内容 |
| Java |
名义子类型 |
| TypeScript |
结构子类型 |
研究前沿
1. F-有界多态性
实现陷阱
| 陷阱 |
实际后果 |
解决方案 |
| 传递性 |
不健全性 |
证明引理 |