Counterexamples in type systems (2021)

背景

类型系统是现代编程语言的核心基础设施，其根本目标是在程序执行前捕获类型错误，同时尽可能减少对程序员的约束。然而，类型系统的设计始终面临表达力与安全性之间的张力：过于严格的类型系统会阻碍合理的编程模式，过于宽松则可能漏检真正的错误。

Stephen Dolan 整理的《Counterexamples in Type Systems》是一篇独特的文献，它不展示类型系统如何成功，而是系统性地收集类型系统可能失败的各种场景。这些反例来自类型理论、编译器实现和实际编程语言的交互，揭示了即使经过严格形式化验证的类型系统，也可能存在微妙的漏洞或违反直觉的行为。

核心内容

本文档按主题分类整理了31个类型系统反例，每个反例都指向类型系统理论或实现中的特定缺陷：

多态与变型问题

• Polymorphic references：多态引用导致的类型不安全，典型场景是可变引用与参数多态的交互
• Covariant containers：协变容器在允许写入时破坏类型安全
• Incomplete variance checking：编译器对变型（variance）检查不完整，遗漏某些不安全场景

构造与递归

• Objects under construction：对象构造过程中暴露未完全初始化的状态
• Curry's paradox：利用递归类型构造逻辑悖论，导致类型系统不一致
• Eventually, nothing：类型推导最终产生无意义的底类型（bottom type）

类型推断与证据

• Dubious evidence：类型推断器生成看似合理但实际错误的类型证据
• Some kinds of Anything：Any 类型在不同上下文中的语义不一致
• Any (single) thing：单一 Any 类型与多态性的交互问题
• Mutable matching：对可变值进行模式匹配时的类型精化失效

运行时与重载

• Runtime type misinformation：运行时类型信息与静态类型声明不符
• Overloading and polymorphism：重载解析与多态推断的交互冲突

类型唯一性与区分

• Distinctness I: Injectivity：类型构造器非单射导致不同类型被错误识别为相同
• Distinctness II: Recursion：递归类型的唯一性判定问题
• Distinctness III: Options：可选类型（Option）与可空类型的混淆

子类型与继承

• Subtyping vs. inheritance：子类型关系与类继承关系的不一致
• Selfishness：子类型化中"自私"的类型转换规则
• Privacy violation：私有成员通过类型系统漏洞被外部访问

类型表达式稳定性

• Unstable type expressions：类型表达式在求值过程中不稳定，导致类型依赖时序
• The avoidance problem：类型系统无法避免某些病态类型构造
• A little knowledge...：类型推断器基于不完整信息做出错误决策

递归类型

• Underdetermined recursion：递归类型约束不足，允许不一致的解
• Overdetermined recursion：递归类型约束过度，排除合法的程序
• Scope escape：类型变量意外逃逸其作用域
• Under false pretenses：类型在虚假假设下被接受

高级类型特性

• Suspicious subterms：类型项中的可疑子结构
• There's only one Leibniz：莱布尼茨等式（Leibniz equality）的唯一性问题
• Intersecting references：引用相交导致的类型冲突
• Polymorphic union refinement：多态联合类型的细化问题
• Positivity, strict and otherwise：正性条件（positivity condition）的严格与非严格解释
• Nearly-universal quantification：近乎全称量化的边界情况

关键要点

• 类型系统的安全性不是绝对的，而是依赖于对特定编程模式的假设
• 多态性、递归、子类型化和类型推断的组合可能产生意外的交互问题
• 编译器实现中的变型检查、作用域管理和唯一性判定是常见的错误来源
• 运行时类型信息与静态类型系统的不一致会破坏类型安全保证
• 类型系统的形式化验证需要覆盖这些边界情况，而非仅