The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose $F^\omega_{..}$, a rigorous theoretical foundation for Scala's higher-kinded types. $F^\omega_{..}$ extends $F^\omega_{<:}$ with interval kinds, which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of $F^\omega_{..}$, as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.
翻译：依附物体类型(DOT)的计算法使得Scala能够更有原则、更有力地实施Scala,但事实证明它对类型计算的支持不够。作为一种补救办法,我们提议美元,作为Scala较高种类的严格理论基础。$F ⁇ omega*。}美元延展了美元(F ⁇ omega}):美元与间隔种类:美元,它提供了对Scala所发现的重要类型和类型级抽象机制的统一处理,如约束量化、约束操作者抽象、半透明类型定义和一级分型限制。结果产生了高排序分型的灵活和一般理论。我们证明了美元(F ⁇ omega}.})的类型和种类安全性,以及亚型类型不健全和不可避免性。我们在Agda采用基于世系替代的完全合成方法,所有证据都在Agda被机械化。
相关内容
微信扫码咨询专知VIP会员