一句话：通过略微松弛参数性，给出支持参数多态的空间高效渐进类型强制转换演算与保持语义的翻译。
渐进类型允许同一程序中混合已标注与未标注的代码，其高效实现一直是活跃的研究课题。本文研究存在参数多态时渐进类型的空间高效（space-efficient）问题。已有工作证明：若要求完全参数性，支持参数多态的空间高效实现在原则上不可能。本文则表明，只要略微松弛参数性，空间高效实现是可能的。作者首先定义强制转换演算 λC^mp_∀，其多态性是「大部分参数性」（mostly parametric），并刻画其所满足的松弛参数性；随后给出其空间高效版本 λS^mp_∀，证明 λS^mp_∀ 的程序可以空间高效地执行，并证明从 λC^mp_∀ 到 λS^mp_∀ 的翻译既保持类型也保持语义。
Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficient problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop λC m p ∀ , which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present λS m p ∀ , a space-efficient version of λC m p ∀ , and prove that λS m p ∀ programs can be executed in a space-efficient manner and that translation from λC m p ∀ to λS m p ∀ is type-and semantics-preserving.
@article{IgarashiOST24,
title = {Space-Efficient Polymorphic Gradual Typing, Mostly Parametric},
author = {Atsushi Igarashi and Shota Ozaki and Taro Sekiyama and Yudai Tanabe},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656441}
}