Non-parametric parametricity

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 a novel "polarized" form of our logical relation, which enables us to distinguish formally between positive and negative notions of parametricity.

REFERENCES

• 1: Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didier Remy. Dynamic typing in polymorphic languages. JFP, 5(1):111--130, 1995.
• 2: Amal Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004.
• 3: Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006.
• 4: Amal Ahmed. Personal communication, 2009.
• 5: Amal Ahmed and Matthias Blume. Typed closure conversion preserves observational equivalence. In ICFP, 2008.
• 6: Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In POPL, 2009.
• 7: Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657--683, 2001.
• 8: Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin. 2007.
• 9: Jean-Yves Girard. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. PhD thesis, Universite Paris VII, 1972.
• 10: Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic type abstraction. TOPLAS, 22(6):1037--1080, 2000.
• 11: Robert Harper and John C. Mitchell. Parametricity and variants of Girard's J operator. Information Processing Letters, 1999.
• 12: Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In POPL, 1995.
• 13: JacobMatthews and Amal Ahmed. Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In ESOP, 2008.
• 14: John C. Mitchell. Representation independence and data abstraction. In POPL, 1986.
• 15: John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. TOPLAS, 10(3):470--502, 1988.
• 16: Georg Neis. Non-parametric parametricity. Master's thesis, Universitat des Saarlandes, 2009.
• 17: Andrew Pitts. Typed operational reasoning. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 7. MIT Press, 2005.
• 18: Andrew Pitts and Ian Stark. Observable properties of higher order functions that dynamically create local names, or: What's new? In MFCS, volume 711 of LNCS, 1993.
• 19: Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In HOOTS, 1998.
• 20: John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.
• 21: Andreas Rossberg. Generativity and dynamic opacity for abstract types. In PPDP, 2003.
• 22: Andreas Rossberg. Dynamic translucency with abstraction kinds and higher-order coercions. In MFPS, 2008.
• 23: Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, and Gert Smolka. Alice ML through the looking glass. In TFP, volume 5, 2004.
• 24: Peter Sewell. Modules, abstract types, and distributed versioning. In POPL, 2001.
• 25: Peter Sewell, James Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, and Viktor Vafeiadis. Acute: High-level programming language design for distributed computation. JFP, 17(4&5):547--612, 2007.
• 26: Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. JCS, 11(4):521--554, 2003.
• 27: Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. TCS, 375(1-3):161--192, 2007.
• 28: Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. JACM, 54(5):1--43, 2007.
• 29: Dimitrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An open and shut typecase. In TLDI, 2005.
• 30: Philip Wadler. Theorems for free! In FPCA, 1989.
• 31: Geoffrey Washburn and Stephanie Weirich. Generalizing parametricity using information flow. In LICS, 2005.
• 32: Stephanie Weirich. Type-safe cast. JFP, 14(6):681--695, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
intensional type analysis, parametricity, representation independence, step-indexed logical relations, type-safe cast