Mathematical Structures in Computer Science



Parametric polymorphism and operational equivalence


ANDREW M. PITTS a1
a1 Cambridge University Computer Laboratory, Pembroke Street, Cambridge, CB2 3QG, UK

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’) data types. 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 [for all]-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.

(Received December 18 1998)
(Revised September 28 1999)