一句话:提出了一个能忠实表达 Reynolds 原始关系参数性理论的一般框架。
Reynolds 最初的关系参数性理论旨在刻画多态 System F 程序保持输入之间所有关系这一现象。但他后来表明,该理论只能在具有非直谓宇宙的元理论中表述,例如归纳构造演算。此后出现了若干更抽象的关系参数性处理方式;本文表明,这些处理似乎都无法令人满意地表达 Reynolds 的原始理论。为此,本文提出一个通用框架来刻画关系参数性,并据此分析既有抽象方法的局限,目标是在合适的元理论中忠实复现 Reynolds 原始理论的核心思想。
Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in a metatheory with an impredicative universe, such as the Calculus of Inductive Constructions. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these seem to express Reynolds' original theory in a satisfactory way.