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
forall-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.