Type soundness for dependent object types (DOT)
Type soundness for dependent object types (DOT)
复制标题
依赖对象类型 (DOT) 的类型健全性
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Nada Amin
中科院分区：
文献类型：
--
作者：
Tiark Rompf;Nada Amin
Scala的类型系统统一了ML模块、面向对象和函数式编程的各个方面.依赖对象类型（DOT）演算家族已经被提出作为Scala和类似表达语言的新理论基础。不幸的是，类型可靠性只建立在DOT的有限子集上。事实上，重要的Scala特性，如类型细化或子类型与格结构的关系，至少破坏了一个关键的元理论属性，如环境缩小或可逆子类型传递性，这通常是类型可靠性证明所需的。本文的主要贡献是演示如何，也许令人惊讶的是，即使这些属性失去了其充分的普遍性，丰富的DOT演算，包括递归类型的细化和子类型格与交叉类型仍然可以被证明是合理的。关键的见解是，子类型传递性只需要在运行时执行的代码路径中可逆，上下文完全由有效的运行时对象组成，而不一致的子类型上下文可以被允许用于从未执行的代码。
Scala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for restricted subsets of DOT. In fact, it has been shown that important Scala features such as type refinement or a subtyping relation with lattice structure break at least one key metatheoretic property such as environment narrowing or invertible subtyping transitivity, which are usually required for a type soundness proof. The main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a rich DOT calculus that includes recursive type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that subtyping transitivity only needs to be invertible in code paths executed at runtime, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.