Studies of the mathematical properties of
impredicative polymorphic types have for the most part focused on
the <I>polymorphic lambda calculus</I> of Girard-Reynolds, which is
a calculus of <i>total</i> 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
<I>relational parametricity</I> 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.