Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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 Jamil Ahmed, Semantics of types for mutable state, Princeton University, Princeton, NJ, 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 , Matthias Blume, Typed closure conversion preserves observational equivalence, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 6: Amal Ahmed , Derek Dreyer , Andreas Rossberg, State-dependent representation independence, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 7: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 8: Karl Crary , Robert Harper, Syntactic Logical Relations for Polymorphic and Recursive Types, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.259-299, April, 2007 [doi>10.1016/j.entcs.2007.02.010]
• 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 , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 11: Robert Harper , John C. Mitchell, Parametricity and variants of Girard's J operator, Information Processing Letters, v.70 n.1, p.1-5, April 01, 1999 [doi>10.1016/S0020-0190(99)00036-8]
• 12: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 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, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 15: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 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 M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 19: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 20: John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.
• 21: Andreas Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.241-252, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888274]
• 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, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-247, January 2001, London, United Kingdom
• 25: PETER SEWELL , JAMES J. LEIFER , KEITH WANSBROUGH , FRANCESCO ZAPPA NARDELLI , MAIR ALLEN-WILLIAMS , PIERRE HABOUZIT , VIKTOR VAFEIADIS, Acute: High-level programming language design for distributed computation, Journal of Functional Programming, v.17 n.4-5, p.547-612, July 2007 [doi>10.1017/S0956796807006442]
• 26: Eijiro Sumii , Benjamin C. Pierce, Logical relation for encryption, Journal of Computer Security, v.11 n.4, p.521-554, July 2003
• 27: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, v.375 n.1-3, p.169-192, April, 2007 [doi>10.1016/j.tcs.2006.12.032]
• 28: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Journal of the ACM (JACM), v.54 n.5, p.26-es, October 2007 [doi>10.1145/1284320.1284325]
• 29: Dimitrios Vytiniotis , Geoffrey Washburn , Stephanie Weirich, An open and shut typecase, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.13-24, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040296]
• 30: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• 31: Geoffrey Washburn, Generalizing Parametricity Using Information-flow, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.62-71, June 26-29, 2005 [doi>10.1109/LICS.2005.20]
• 32: Stephanie Weirich, Type-FUNCTIONAL PEARL safe cast, Journal of Functional Programming, v.14 n.6, p.681-695, November 2004 [doi>10.1017/S0956796804005179]

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