Theorems for Free!

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 Gira...

• Type: Conference
• Year: 1989
• Where: FPCA
• Authors: Philip Wadler
• Keywords: FPCA 1989, Free Theorems, Logical Relation, Parametricity Theorem, Programming Languages