一句话：提出改进的多态 blame 演算，用步进索引 Kripke 逻辑关系证明关系参数性，并导出两个自由定理。
多态 blame 演算将静态类型（含全称类型）与动态类型结合，核心挑战是即使动态类型代码被转换到全称类型也保持参数性。此前工作用运行时类型生成保持参数性，但证明缺失或存在缺陷。本文提出改进的多态 blame 演算，证明其满足关系参数性。证明使用步进索引 Kripke 逻辑关系；步进索引用于使动态类型情形下逻辑关系良定义，可能世界记录生成类型名到类型以及类型名到关系的映射。作者证明基本性质，并证明其相对上下文等价可靠。最后导出两个自由定理来展示参数性的效用。
The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.
@article{AhmedJSW17,
title = {Theorems for free for free: parametricity, with and without types},
author = {Amal Ahmed and Dustin Jamner and Jeremy G. Siek and Philip Wadler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110283}
}