parametric polymorphism and operational equivalence

See an old friend (polymorphic lambda calculus) in a new light by
reading the following preprint, available as


  Parametric Polymorphism and Operational Equivalence
  (Preliminary Version)

  Andrew M. Pitts
  Cambridge University Computer Laboratory
  Pembroke Street, Cambridge CB2 3QG, UK


  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.