一句话：提出更语义化的渐进类型解释，并用 subtyping 与 materialization 统一渐进化三种多态类型系统。
论文重新审视渐进类型，提出一种更具语义色彩的解释：渐进类型并非只是未知类型标记，而由类型间关系来刻画。作者据此将两类多态——子类型多态与隐式参数多态——渐进化。他们用子类型（subtyping）和 materialization 两个 preorder 统一刻画三个渐进类型系统：Hindley-Milner、带子类型，以及带并集与交集类型。每个系统均给出声明式与算法式定义：声明式版本通过添加两条类 subsumption 规则，使定义更清晰、可理解且简洁；算法式版本则复用统一（unification）与 tallying 等已有技术。该工作为渐进类型提供了更统一的语义视角，并展示了多态类型系统渐进化的系统化路径。
We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type systems ---Hindley-Milner, with subtyping, and with union and intersection types--- in terms of two preorders, subtyping and materialization. We define these systems both declaratively ---by adding two subsumption-like rules--- which yields clearer, more intelligible, and streamlined definitions, and algorithmically by reusing existing techniques such as unification and tallying.
@article{paperbot619,
title = {Gradual typing: a new perspective},
author = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G. Siek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290329}
}