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.