[Prev][Next][Index][Thread]
parametric polymorphism and operational equivalence
See an old friend (polymorphic lambda calculus) in a new light by
reading the following preprint, available as
ftp://ftp.cl.cam.ac.uk/papers/ap/parpoe.ps
Parametric Polymorphism and Operational Equivalence
(Preliminary Version)
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 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 operationally-based approach to Reynolds'
notion of relational parametricity is developed for an extension of
Plotkin's PCF with forall-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.