Karl Crary
ABSTRACT
Many properties of parametric, polymorphic functions can be determined simply by inspection of their types. Such results are usually proven using Reynolds's parametricity theorem. However, Reynolds's theorem can be difficult to show in some settings, particularly ones involving computational effects. I present an alternative technique for proving some parametricity results. This technique is considerably simpler and easily generalizes to effectful settings. It works by instantiating polymorphic functions with singleton types that fully specify the behavior of the functions. Using this technique, I show that callers' stacks are protected from corruption during function calls in Typed Assembly Language programs.
- 1.Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. In Theoretical Aspects of Computer Software 1991, volume 526 of Lecture Notes in Computer Science, pages 750-770, Sendai, Japan, 1991. Springer-Verlag. Google Scholar
Digital Library
- 2.Andrew J. Kennedy. Relational parametricity and units of measure. In Twenty-Fourth A CM Symposium on Principles of Programming Languages, pages 442-455, Paris, January 1997. Google ScholarDigital Library
- 3.QingMing Ma. Parametricity as subtyping. In Nineteenth A CM Symposium on Principles of Programming Languages, pages 281-292, Albuquerque, New Mexico, January 1992. Google ScholarDigital Library
- 4.QingMing Ma and John C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In Seventh Mathematical Foundations o/Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 1-40, Pittsburgh, Pennsylvania, March 1991. Sprlnger-Verlag. Google ScholarDigital Library
- 5.Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In Second Workshop on Types in Compilation, voI- ume 1473 of Lecture Notes in Computer Science. Springer-Verlag, March 1998. Extended version published as CMU technical report CMU-CS-98- 178. Google ScholarDigital Library
- 6.Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. A CM Transactions on Programming Languages and Systems, 1999. To appear. An earlier version appeared in the 1998 Symposium on Principles of Programming Languages. Google ScholarDigital Library
- 7.Peter W. O'Hearn and Robert D. Tennent. Parametricity and local variables. Journal of the A CM, 42(3):658-709, May 1995. Google ScholarDigital Library
- 8.Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In International Conference on Typed Lambda Calculi and Applications, pages 361-375, 1993. Google ScholarDigital Library
- 9.Gordon Plotkin, Martin Abadi, and Luca Cardelli. Subtyping and parametricity. In Ninth IEEE Symposium on Logic in Computer Science, pages 310- 319, July 1994.Google ScholarCross Ref
- 10.John C. Reynolds. Types, abstraction and parametric polymorphism. In information Processing '83, pages 513-523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.Google Scholar
- 11.Chistopher Strachey. Fundamental concepts in programming languages. Lecture Notes, International Summer School in Computer Programming, Copenhagen, August 1967.Google Scholar
- 12.Philip Wadler. Theorems for free! In Fourth Conference on Functional Programming Languages and Computer Architecture, London, September 1989. Google ScholarDigital Library
- 13.Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115:38-94, 1994. Google ScholarDigital Library
Index Terms
- A simple proof technique for certain parametricity results
Recommendations
A simple proof technique for certain parametricity results
Many properties of parametric, polymorphic functions can be determined simply by inspection of their types. Such results are usually proven using Reynolds's parametricity theorem. However, Reynolds's theorem can be difficult to show in some settings, ...
Gradual parametricity, revisited
Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently ...
Parametricity as subtyping
POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesA polymorphic function is parametric if it has uniform behavior for all type parameters. This property is useful when writing, reasoning about, and compiling functional programs.
We show how to syntactically define and reason about parametricity in a ...
Comments