DOT的案例：具有模式匹配和GADT风格推理的对象的理论基础
摘要：泛型类层次结构上的模式匹配在许多面向对象的编程语言中得到了支持，如Scala、Ceylon、Java、Kotlin、TypeScript和Flow。然而，大多数这些语言中的模式匹配在泛型类层次结构上会导致令人困惑的类型错误。然而，在许多场景下，比如操作有类型的AST时，这些特性的组合是自然而然的。为了正确支持它，编译器需要实现子类型重构的形式：在模式匹配期间在运行时重建发现的子类型信息的能力。我们引入了cDOT，这是一种新的Dependent Object Types(DOT)系列的演算法，旨在作为子类型重构的形式基础。作为Scala的形式基础的pDOT的子孙，cDOT可以用来对高级面向对象的特性进行编码，如泛型继承、类型构造器变异、F-bound多态和一流递归模块。我们通过将$lambda_{2,Gmu}$，一种经典的基于约束的GADT演算法，编码到cDOT中，证明了子类型重构包含GADTs。
作者：Aleksander Boruch-Gruszecki, Rados{l}aw Wa''sko, Yichen Xu, Lionel Parreaux
论文ID：2209.07427
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-02-24