论文标题
DOT的案例：具有模式匹配和GADT式推理的对象的理论基础
A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning
论文作者
论文摘要
现在，OO传统中的许多编程语言都以某种形式支持模式匹配。历史示例包括Scala和Ceylon，以及Java，Kotlin，Typescript和Flow的最新添加。但是，在通用类层次结构上匹配的模式匹配当前会导致大多数此类语言中令人困惑的类型错误。然而，这种特征的组合在许多情况下自然发生，例如在操纵键入AST时。为了正确支持它，编译器需要实现一种亚型重建形式：在模式匹配期间在运行时发现的子类型信息的能力。我们介绍了CDOT，这是一个依赖对象类型（DOT）家族中的新微积分（DOT），旨在作为亚型重建的正式基础。 CDOT从PDOT中降为PDOT，本身是Scala的正式基础，可用于编码高级面向对象的特征，例如通用继承，类型的构造函数方差，F-BOND-BOND-BOND-BOND-BOND OD-OD-COND cONDER-CONDER-OR-OR-OR-OR-ORYMORMORISP和一流的递归模块。我们证明了通过编码$λ_{2，gμ} $（基于经典约束的Gadt cyculus）将亚型重建的元素归为gadts。
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 need 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.
