Department of Computer Science and Technology

Technical reports

Parametric polymorphism and operational equivalence

Andrew M. Pitts

December 1998, 39 pages

DOI: 10.48456/tr-454

Abstract

Studies of the mathematical properties of impredicative polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard-Reynolds, which is a calculus of total polymorphic functions. This paper considers polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (‘lazy’) datatypes. An approach to Reynolds’ notion of relational parametricity is developed that works directly on the syntax of a programming language, using a novel closure operator to relate operational behaviour to parametricity properties of types. Working with an extension of Plotkin’s PCF with ∀-types, lazy lists and existential types, we show by example how the resulting logical relation can be used to prove properties of polymorphic types up to operational equivalence.

Full text

PDF (2.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-454,
  author =	 {Pitts, Andrew M.},
  title = 	 {{Parametric polymorphism and operational equivalence}},
  year = 	 1998,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-454.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-454},
  number = 	 {UCAM-CL-TR-454}
}