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.