Free Theorems in the Presence of seq

Patricia Johann and Janis Voigtlaender

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


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.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Start Conference Manager
Conference Systems