一句话：提出带区间 kind 的 F··ω，为 Scala 高阶类型提供统一的子类型理论基础。
针对 DOT 对类型级计算支持不足的问题，论文提出 F··ω，作为 Scala 高阶类型（higher-kinded types）的严谨理论基础。它在 F<:ω 上引入区间 kind（interval kinds），以统一方式刻画 Scala 中重要的类型层与 kind 层抽象机制，包括有界量化、有界算子抽象、半透明类型定义和一等子类型约束，从而形成灵活而通用的高阶子类型理论。作者证明 F··ω 的类型与 kind 安全性、类型的弱规范化以及子类型判定的不可判定性，并在 Agda 中采用基于 hereditary substitution 的完全语法方法机器化全部证明。
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 ·· ω , a rigorous theoretical foundation for Scala’s higher-kinded types. F ·· ω extends F <: ω 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 ·· ω , 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.
@article{paperbot1133,
title = {A theory of higher-order subtyping with type intervals},
author = {Sandro Stucki and Paolo G. Giarrusso},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473574}
}