摘要
Type abstraction and intensional type analysis are features seemingly at odds-type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implemented "dynamic type generation" as a way to reconcile these features. The idea is that, when one defines an abstract type, one should also be able to generate at run time a fresh type name, which may be used as a dynamic representative of the abstract type for purposes of type analysis. The question remains: in a language with non-parametric polymorphism, does dynamic type generation provide us with the same kinds of abstraction guarantees that we get from parametric polymorphism?
Our goal is to provide a rigorous answer to this question. We define a step-indexed Kripke logical relation for a language with both non-parametric polymorphism (in the form of type-safe cast) and dynamic type generation. Our logical relation enables us to establish parametricity and representation independence results, even in a non-parametric setting, by attaching arbitrary relational interpretations to dynamically-generated type names. In addition, we explore how programs that are provably equivalent in a more traditional parametric logical relation may be "wrapped" systematically to produce terms that are related by our non-parametric relation, and vice versa. This leads us to a novel "polarized" form of our logical relation, which enables us to distinguish formally between positive and negative notions of parametricity.
摘要译文
类型抽象和内涵类型分析似乎是不相容的特征，旨在保证参数和表示的独立性，而类型分析本质上是非参数的。然而，最近有几位研究人员提出并实施了“动态类型生成”作为调和这些特征的一种方式。这个想法是，当定义一个抽象类型时，还应该能够在运行时生成一个新的类型名称，为了进行类型分析，可以将其用作抽象类型的动态代表。问题依然存在：在非参数多态的语言中，动态类型生成是否为我们提供了与参数多态相同的抽象保证？我们的目标是为这个问题提供一个严格的答案。我们定义了一个具有非参数多态性（以类型安全转换形式）和动态类型生成的语言的逐步索引Kripke逻辑关系。我们的逻辑关系使我们能够建立参数性和表示独立性结果，即使在非参数设置中，通过将任意的关系解释附加到动态生成的类型名称。此外，我们探讨如何在一个更传统的参数化逻辑关系中证明是等价的程序可以被系统地“包装”来产生与我们的非参数关系相关的术语，反之亦然。这导致了我们的逻辑关系的一种新的“极化”形式，这使我们能够正式地区分参数性的正面和负面的概念。
Georg Neis[1];Derek Dreyer[1];Andreas Rossberg[1]. Non-parametric parametricity[J]. ACM SIGPLAN Notices, 2009,44(9): 135-148