一句话：提出 cDOT 演算，为对象语言中的子类型重建提供形式基础，并将 GADT 风格推理编码进来。
许多面向对象语言已支持某种形式的模式匹配，但在泛型类层次上进行模式匹配时，编译器常给出令人困惑的类型错误。其关键需求是子类型重建：在模式匹配中利用运行时揭示的子类型信息来恢复静态类型关系。为此，论文提出 cDOT，一种属于 Dependent Object Types (DOT) 家族的新演算，作为子类型重建的形式基础。cDOT 继承 pDOT（Scala 的形式基础），可编码泛型继承、类型构造子型变、F-bounded 多态和一等递归模块等高级 OO 特性。作者进一步证明子类型重建可以涵盖 GADTs，将经典基于约束的 GADT 演算 λ2,Gµ 编码到 cDOT 中。
Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies currently results in puzzling type errors in most of these languages. Yet this combination of features occurs naturally in many scenarios, such as when manipulating typed ASTs. To support it properly, compilers needs to implement a form of subtyping reconstruction: the ability to reconstruct subtyping information uncovered at runtime during pattern matching. We introduce cDOT, a new calculus in the family of Dependent Object Types (DOT) intended to serve as a formal foundation for subtyping reconstruction. Being descended from pDOT, itself a formal foundation for Scala, cDOT can be used to encode advanced object-oriented features such as generic inheritance, type constructor variance, F-bounded polymorphism, and first-class recursive modules. We demonstrate that subtyping reconstruction subsumes GADTs by encoding λ 2, G µ , a classical constraint-based GADT calculus, into cDOT.
@article{paperbot1443,
title = {A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning},
author = {Aleksander Boruch-Gruszecki and Radosław Waśko and Yichen Xu and Lionel Parreaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563342}
}