Parametric Polymorphism and Operational Equivalence
Andrew M. Pitts,
Cambridge University Computer Laboratory,
Pembroke Street Cambridge CB2 3QG, UK
Abstract
Studies of the mathematical properties of impredicatively 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 talk 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 operationally-based
approach to Reynolds' notion of relational parametricity is developed
for an extension of Plotkin's PCF with universally quantified types
and lazy lists. The resulting logical relation is shown to be a
useful tool for proving properties of polymorphic types up to a notion
of operational equivalence based on Morris-style contextual
equivalence.
[Slides, paper.]