Theorems for Free!

13 years 8 months ago

Download www.iai.uni-bonn.de

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-reﬂecting 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 sufﬁcient 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

Real-time Traffic