Non-Parametric Parametricity
Venue
Journal of Funcitonal Programming, vol. 21 (4 & 5) (2011)
Publication Year
2011
Authors
Georg Neis, Derek Dreyer, Andreas Rossberg
BibTeX
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 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 develop a “polarized” variant of our logical relation, which enables us to
distinguish formally between positive and negative notions of parametricity.
