 |
Non-Parametric Parametricity
Georg Neis, Derek Dreyer and Andreas Rossberg
The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)Edinburgh, Scotland, 31st August - 2nd September 2009
Abstract
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, with a novel form of ``possible world'', for a language with both non-parametric polymorphism 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 distinguishes between positive and negative notions of parametricity.
START Conference Manager (V2.56.8 - Rev. 748M)