一句话：通过显式化类型名生成，提出同时满足渐进性与参数性定理的 System F 渐进扩展。
参数多态与渐进类型的结合一直困难：已有语言无法同时满足参数性和渐进性；Toro 等人猜测，使用动态类型生成的 System F 渐进扩展中二者不可兼得。本文指出，冲突并非来自两个性质本身，而是既有语法结合动态类型生成后被迫进行类型导向计算，这常破坏这两个定理。作者修改全称与存在类型的语法，使类型名生成显式化，从而消除类型导向计算。所得语言运行时语义简单，并可翻译到静态类型语言，其中动态类型解释为可动态扩展的和类型。结果表明该语言同时满足渐进性和参数性，且参数性可作为渐进性关系解释的直接推论。
Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work. We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.
@article{paperbot538,
title = {Graduality and parametricity: together again for the first time},
author = {Max S. New and Dustin Jamner and Amal Ahmed},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371114}
}