Sciweavers

35
Voted
FPCA
1989

Theorems for Free!

14 years 4 months ago
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...
Philip Wadler
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1989
Where FPCA
Authors Philip Wadler
Comments (0)