Patricia Johann
Rutgers University
Free Theorems in the Presence of seq (joint work with Janis
Voigtlaender)
Abstract:
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