Free theorems in the presence of seq

Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, the standard parametricity theorem fails for nonstrict languages supporting a polymorphic strict evaluation primitive like Haskell's seq. Contrary to the folklore surrounding seq and parametricity, we show that not even quantifying only over strict and bottom-reflecting relations in the -clause of the underlying logical relation -- and thus restricting the choice of functions with which such relations are instantiated to obtain free theorems to strict and total ones -- is sufficient to recover from this failure. By addressing the subtle issues that arise when propagating up the type hierarchy restrictions imposed on a logical relation in order to accommodate the strictness primitive, we provide a parametricity theorem for the subset of Haskell corresponding to a Girard-R...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Janis Voigtländer, Patricia Johann
• Keywords: Familiar Program Transformations, Free Theorems, Logical Relation, POPL 2004, Programming Languages