一句话：用软契约验证静态分析无类型代码，在编译期消除渐进类型边界的绝大多数动态检查，从而消除性能开销。
渐进类型允许在无类型程序中逐步加入静态类型，但为保证健全性，语言必须在类型化与无类型代码的边界插入运行时检查，已有性能研究表明其开销可能高得惊人，令人质疑健全渐进类型的可行性。本文基于既有的“软契约验证”（soft contract verification）工作，提出一个关键洞见：虽然渐进类型系统不能信任无类型代码，但优化时也无需只考虑最坏情况；可以对渐进类型程序中的无类型部分做静态分析，证明渐进类型边界所隐含的动态检查实际上不会失败，从而在编译期将其消除。该分析是模块化的，可应用于程序的任意部分。作者在十二个此前被证明具有不可接受性能开销的渐进类型程序上进行评估：这些程序原中位开销为 2.5 倍、最坏高达 80.6 倍，本文方法在多数情况下完全消除开销，最坏情形下也仅剩 1.5 倍开销。
Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead. Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program. We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—with a median overhead of 2.5× and up to 80.6× in the worst case—and eliminate all overhead in most cases, suffering only 1.5× overhead in the worst case.
@article{paperbot1177,
title = {Corpse reviver: sound and efficient gradual typing via contract verification},
author = {Cameron Moy and Phúc C. Nguyễn and Sam Tobin-Hochstadt and David Van Horn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434334}
}