Martín Abadi
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 ℜ. Girard's system F deals with terms and types; ℜ is an extension of F that deals also with relations between types.
In ℜ, 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 ∀(X)X → 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.
- Bainbridge, et al 1990.E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott, Functoriai polymorphism. Theoretical Computer Science 70, 35-64. Google Scholar
Digital Library
- Böhm, Berarducci 1985.C. BOhm and A. Berarducci, Automatic synthesis of typed Z,-programs on term algebras. Theoretical Computer Science 39, 135-154.Google Scholar
- Cardelli, et al 1991.L. CardeUi, J.C. Mitchell, S. Martini, and A. Scedrov. An extension of system F with subtyping. Proc. Theoretical Aspects of Computer Software. Sendai, Japan. Lecture Notes in Computer Science 526. Springer-Verlag. Google ScholarDigital Library
- Girard, Lafont, Taylor 1989.J.-Y. Girard, Y. Lafont, and P. Taylor, Proofs and types. Cambridge University Press. Google ScholarDigital Library
- Hasegawa 1991.R. Hasegawa. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. Proc. Theoretical Aspectes of Computer Software. Lecture Notes in Computer Science 526. Springer-Verlag. Google ScholarDigital Library
- Hasegawa 1992.R. Hasegawa, Categorical data types in parametric polymorphism. Manuscript.Google Scholar
- Hyland, Robinson, Rosolini 1990.J.M.E. Hyland, E.P. Robinson, and G. Rosolini. Algebraic types in PER models. Proc. Mathematical Foundations of Programming Semantics. Lecture Notes in Computer Science 442. Springer-Verlag. Google ScholarDigital Library
- Longo, Milstead, Soloviev 1992.G. Longo, C. Milstead, and S. Soloviev, A syntactic understanding of parametricity in polymorphic languages. Manuscript.Google Scholar
- Longo, Moggi 1991.G. Longo and E. Moggi, Constructive natural deduction and its 'obset' interpretation. Mathematical Structures in Computer Science 1(2).Google Scholar
- Ma 1992.Q.M. Ma. Parametricity as subtyping. Proc. 19th Annual ACM Symposium on Principles of Programming Languages. Google ScholarDigital Library
- Ma, Reynolds 1991.Q.M. Ma and J. Reynolds. Types, abstraction, and parametric polymorphism, part 2. Proc. Mathematical Foundations of Programming Semantics. Springer-Verlag. Google ScholarDigital Library
- Mairson 1991.H. Mairson. Outline of a proof theory of parametricity. Proc. 5th International Symposium on Functional Programming Languages and Computer Architecture. Springer-Verlag. Google ScholarDigital Library
- Milner, Tofte, Harper 1989.R. Milner, M. Toftc, and R. Harper, The dermition of Standard ML. MIT Press. Google ScholarDigital Library
- Mitchell, Scedrov 1992.J.C. Mitchell and A. Scedrov, Sconing, relators, and parametricity. Manuscript.Google Scholar
- Plotkin, Abadi, Cardelli 1992.G.D. Plotkin, M. Abadi, and L. Cardelli, A logic for parametric polymor. phism. Manuscript.Google Scholar
- Reynolds 1983.J.C. Reynolds, Types, abstraction, and parametric polymorphism, in Information Processing, R.E.A. Mason, Editor. North Holland: p. 513-523.Google Scholar
- Strachey 1967.C. Strachey, Fundamental concepts in programming languages. Lecture notes for the International Summer School in Computer Programming, Copenhagen, August 1967.Google Scholar
- Wadler 1989.P. Wadler. Theorems for free! Proc. 4th International Symposium on Functional Programming Languages and Computer Architecture. Springer- Verlag.Google Scholar
- Wadler 1991.P. Wadler, Recursive types for free! Manuscript.Google Scholar
Recommendations
Theorems for free!
FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architectureOn understanding types, data abstraction, and polymorphism
The MIT Press scientific computation seriesOur objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the relevance of recent research to the design of practical ...
Intrinsically-typed definitional interpreters for imperative languages
A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a ...
Comments