一句话：提出 vigilance，判定渐进类型语言的检查注入与动态语义是否充分执行静态类型系统，并比较 Natural 与 Transient。
渐进类型中，同一程序在不同语言里会因动态检查策略不同而产生不同行为，即使静态类型系统相同。已有类型可靠性、完全监控等性质不能充分回答：检查注入翻译与动态语义的组合是否足够执行静态类型系统。本文提出 vigilance，一种语义分析工具，要求二者组合能够执行值在运行时的完整类型历史，即与该值关联的所有类型。作者证明：Natural 渐进类型的标准组合对简单类型系统是 vigilance 的，而 Transient 不是；反之，Transient 对标签类型系统是 vigilance 的，而 Natural 不是。这厘清了两大可靠渐进类型进路的类型级推理能力。最后，文章展示 vigilance 如何指导设计，提出并研究新的静态渐进类型系统 truer，它强于标签类型并更忠实反映 Transient 动态语义能保证的类型级推理能力。
In gradual typing, different languages perform different dynamic type checks for the same program even though the languages have the same static type system. This raises the question of whether, given a gradually typed language, the combination of the translation that injects checks in well-typed terms and the dynamic semantics that determines their behavior sufficiently enforce the static type system of the language. Neither type soundness, nor complete monitoring, nor any other meta-theoretic property of gradually typed languages to date provides a satisfying answer. In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting translation and dynamic semantics of a gradually typed language are adequate for its static type system. Technically, vigilance asks if a given translation-and-semantics combination enforces the complete run-time typing history of a value, which consists of all of the types associated with the value. We show that the standard combination for so-called Natural gradual typing is vigilant for the standard simple type system, but the standard combination for Transient gradual typing is not. At the same time, the standard combination for Transient is vigilant for a tag type system but the standard combination for Natural is not. Hence, we clarify the comparative type-level reasoning power between the two most studied approaches to sound gradual typing. Furthermore, as an exercise that demonstrates how vigilance can guide design, we introduce and examine a new theoretical static gradual type system, dubbed truer, that is stronger than tag typing and more faithfully reflects the type-level reasoning power that the dynamic semantics of Transient gradual typing can guarantee.
@article{paperbot2526,
title = {Gradually Typed Languages Should Be Vigilant!},
author = {Olek Gierczak and Lucy Menon and Christos Dimoulas and Amal Ahmed},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649842}
}