Formal parametric polymorphism

ABSTRACT

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In this paper, we develop a syntactic approach to parametricity, and a formal system that embodies this approach: system R . Girard's system F deals with terms and types; R is an extension of F that deals also with relations between types. In R **, it is possible to derive theorems about functions from their types, or “theorems for free”, as Wadler calls them. An easy “theorem for free” asserts that the type ∀XX→ Bool contains only constant functions; this is not provable in F. There are many harder and more substantial examples. Various metatheorems can also be obtained, such as a syntactic version of Reynolds' abstraction theorem.

REFERENCES

• Bainbridge, et al. 1990: E. S. Bainbridge , P. J. Freyd , A. Scedrov , P. J. Scott, Functorial polymorphism, Theoretical Computer Science, v.70 n.1, p.35-64, Jan. 1990 [doi>10.1016/0304-3975(90)90151-7]
• Böhm, Berarducci 1985: C. BOhm and A. Berarducci, Automatic synthesis of typed Z,-programs on term algebras. Theoretical Computer Science 39, 135-154.
• Cardelli, et al. 1991: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An Extension of System F with Subtyping, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.750-770, September 24-27, 1991
• Girard, Lafont, Taylor 1989: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• Hasegawa 1991: Ryu Hasegawa, Parametricity of Extensionally Collapsed Term Models of Polymorphism and Their Categorical Properties, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.495-512, September 24-27, 1991
• Hasegawa 1992: R. Hasegawa, Categorical data types in parametric polymorphism. Manuscript.
• Hyland, Robinson, Rosolini 1990: J. M. E. Hyland , E. P. Robinson , G. Rosolini, Algebraic types in PER models, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.333-350, July 1990, New Orleans, Louisiana, United States
• Longo, Milstead, Soloviev 1992: G. Longo, C. Milstead, and S. Soloviev, A syntactic understanding of parametricity in polymorphic languages. Manuscript.
• Longo, Moggi 1991: G. Longo and E. Moggi, Constructive natural deduction and its 'obset' interpretation. Mathematical Structures in Computer Science 1(2).
• Ma 1992: QingMing Ma, Parametricity as subtyping, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.281-292, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143225]
• Ma, Reynolds 1991: QingMing Ma , John C. Reynolds, Types, Abstractions, and Parametric Polymorphism, Part 2, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.1-40, March 25-28, 1991
• Mairson 1991: Harry G. Mairson, Outline of a proof theory of parametricity, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.313-327, June 1991, Cambridge, Massachusetts, United States
• Milner, Tofte, Harper 1989: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Mitchell, Scedrov 1992: J.C. Mitchell and A. Scedrov, Sconing, relators, and parametricity. Manuscript.
• Plotkin, Abadi, Cardelli 1992: G.D. Plotkin, M. Abadi, and L. Cardelli, A logic for parametric polymor. phism. Manuscript.
• Reynolds 1983: J.C. Reynolds, Types, abstraction, and parametric polymorphism, in Information Processing, R.E.A. Mason, Editor. North Holland: p. 513-523.
• Strachey 1967: C. Strachey, Fundamental concepts in programming languages. Lecture notes for the International Summer School in Computer Programming, Copenhagen, August 1967.
• Wadler 1989: P. Wadler. Theorems for free! Proc. 4th International Symposium on Functional Programming Languages and Computer Architecture. Springer- Verlag.
• Wadler 1991: P. Wadler, Recursive types for free! Manuscript.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics; Syntax

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs; Type structure

General Terms:
Algorithms, Languages, Theory