一句话：将 AGT 的动态检查重构为对子类型关系的抽象解释，并借助前向完备性同时实现空间高效执行与可靠的运行时类型强制。
抽象渐进类型（AGT）是设计渐进类型语言的系统化方法，用其构造的语言自动满足 Siek 等人提出的渐近语言形式语义准则。然而原始 AGT 语义仍有两个重要缺陷：一是运行时检查会破坏正确尾调用，从而丧失底层静态与动态语言原有的空间效率保证；二是运行时检查可能以出人意料的方式无法强制静态类型纪律所要求的模块化不变式，作者在 Garcia 等人的 GTFL≲ 语言中展示了这一点。本文同时解决这两个问题，做法是精化 AGT 动态检查背后的理论：Garcia 等人观察到 AGT 涉及对静态类型的两种抽象，分别用于静态语义与动态语义；作者将后者重新表述为对子类型关系本身的抽象解释，而渐进类型仍抽象静态类型。随后论证 Giacobazzi 与 Quintarelli 提出的前向完备性是同时支持空间高效执行与可靠运行时类型强制的关键。
Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal semantic criteria for gradual languages identified by Siek et al. Nonetheless, vanilla AGT semantics can still have important shortcomings. First, a gradual language's runtime checks should preserve the space-efficiency guarantees inherent to the underlying static and dynamic languages. To the contrary, the default operational semantics of AGT break proper tail calls. Second, a gradual language's runtime checks should enforce basic modular type-based invariants expected from the static type discipline. To the contrary, the default operational semantics of AGT may fail to enforce some invariants in surprising ways. We demonstrate this in the GTFL ≲ language of Garcia et al. This paper addresses both problems at once by refining the theory underlying AGT's dynamic checks. Garcia et al. observe that AGT involves two abstractions of static types: one for the static semantics and one for the dynamic semantics. We recast the latter as an abstract interpretation of subtyping itself, while gradual types still abstract static types. Then we show how forward-completeness (Giacobazzi and Quintarelli) is key to supporting both space-efficient execution and reliable runtime type enforcement.
@article{paperbot1189,
title = {Abstracting gradual typing moving forward: precise and space-efficient},
author = {Felipe Bañados Schwerter and Alison M. Clark and Khurram A. Jafery and Ronald Garcia},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434342}
}