Parametric polymorphism constrains the behavior of functional
programs in a way that allows the derivation of interesting theorems
about them solely from their types, i.e., virtually for free.
It is, however, well known that the standard parametricity theorem
--- which, together with its associated logical relation, provides
the basis for obtaining such free theorems --- fails for lazy
functional languages which support a polymorphic strict evaluation
primitive such as Haskell's seq.
We observe that quantifying only over strict and bottom-reflecting
relations in the forall-clause of the logical relation, and thus
restricting the choice of functions with which such relations are
instantiated to get free theorems to strict and total ones, is
insufficient to recover from this failure. This contradicts what
appears to be the conventional wisdom surrounding seq and
parametricity.
This paper addresses the subtle issues that arise when propagating
up the type hierarchy restrictions imposed on a logical relation in
order to accommodate seq. We prove a parametricity theorem for a
Girard-Reynolds-style calculus with fixpoints, algebraic datatypes,
and seq.
This allows us to enrich standard equational free theorems by
preconditions that guarantee their validity in such a setting.
A particular novelty of our approach is that, under weaker
preconditions, it is also possible to prove ``inequational''
versions of free theorems in the presence of seq. This recovers at
least part of the power of free theorems in situations in which we
would otherwise only be able to observe their failure.
In particular, the inequational free theorems are used to analyze
the impact of seq on familiar program transformations.
