Copenhagen Programming Language Seminar


Free Theorems for Impure Functional Programs

Patricia Johann,
Rutgers University, NJ, USA

Wednesday, June 9, 15:15-16:15
DIKU, Universitetsparken 1, room N010


Parametric polymorphism constrains the behavior of pure functionalprograms 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.

(Joint work with Janis Voigtlaender.)

Scientific host: Fritz Henglein. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org