Patricia Johann
Rutgers University

Free Theorems in the Presence of seq (joint work with Janis Voigtlaender)


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. This observation underlies a number of transformations which can be used to improve the performance of such programs. Unfortunately, the standard parametricity theorem, from which the free theorems guaranteeing correctness of such transformations derives, fails for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq.

Conventional wisdom maintains that quantifying only over strict and bottom-reflecting relations in the forall-clause of the logical relation underlying a parametricity theorem --- 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 the failure of parametricity in the presence of seq.  In this talk I will demonstrate that this conventional wisdom is incorrect, and show how "asymmetric" logical relations can be used to recover parametricity --- and, therefore, free theorems --- when seq is present. I will also show how the resulting "inequational" free theorems can be used to analyze the impact of seq on familiar program transformations.

Host:  Karl Crary
Appointments:  Margaret Weigand

Principles of Programming Seminars

Wednesday, May 19, 2004
3:30 p.m.
Wean Hall 8220