一句话：提出可辩护封存机制与中间语言 Funky，使渐进参数性同时满足参数性与渐进性且不破坏 System F 等价。
渐进类型与参数性难以兼得：渐进地强制参数性需封存值以检测非一致行为，但已有方案或在 System F 中不相容，或放弃 System F 语法并依赖非渐进的用户标注，且都依赖全局动态封存，破坏静态等价。本文提出可辩护封存（plausible sealing），将封存决策推迟到运行时，并设计中间语言 Funky，在多态限于基类型与变量类型实例化的设定下支持该机制。Funky 避免全局动态封存，以受 span 范畴启发的证据表示实现词法作用域封存，并在 Agda 中机器化验证关键引理，证明其同时满足参数性与渐进性且不破坏 System F 等价。本文还给出从 Funk 到 Funky 的翻译，在类型应用受限下建立 Funk 的渐进性，并提供交互式原型。
Graduality and parametricity have proven to be extremely challenging notions to bring together. Intuitively, enforcing parametricity gradually requires possibly sealing values in order to detect violations of uniform behavior. Toro et al. (2019) argue that the two notions are incompatible in the context of System F, where sealing is transparently driven by potentially imprecise type information, while New et al. (2020) reconcile both properties at the cost of abandoning the syntax of System F and requiring user-provided sealing annotations that are not subject to graduality guarantees. Furthermore, all current proposals rely on a global form of dynamic sealing in order to enforce parametric behavior at runtime, which weakens parametric reasoning and breaks equivalences in the static language. Based on the observation that the tension between graduality and parametricity comes from the early commitment to seal values based on type information, we propose plausible sealing as a new intermediate language mechanism that allows postponing such decisions to runtime. We propose an intermediate language for gradual parametricity, Funky, which supports plausible sealing in a simplified setting where polymorphism is restricted to instantiations with base and variable types. We prove that Funky satisfies both parametricity and graduality, mechanizing key lemmas in Agda. Additionally, we avoid global dynamic sealing and instead propose a novel lexically-scoped form of sealing realized using a representation of evidence inspired by the category of spans. As a consequence, Funky satisfies a standard formulation of parametricity that does not break System F equivalences. In order to show the practicality of plausible sealing, we describe a translation from Funk, a source language without explicit sealing, to Funky, that takes care of inserting plausible sealing forms. We establish graduality of Funk, subject to a restriction on type applications, and explain the source-level parametric reasoning it supports. Finally, we provide an interactive prototype along with illustrative examples both novel and from the literature.
@article{paperbot1514,
title = {Plausible sealing for gradual parametricity},
author = {Elizabeth Labrada and Matías Toro and Éric Tanter and Dominique Devriese},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527314}
}