Non-parametric parametricity

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 act type, one should also be able to generate at run time a fresh type name, which may be used as a dynamic representative bstract 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 rela...

• Type: Conference
• Year: 2009
• Where: ICFP
• Authors: Georg Neis, Derek Dreyer, Andreas Rossberg
• Keywords: Dynamic Type Generation, ICFP 2009, Intensional Type Analysis, Programming Languages, Representative Bstract Type