Free Theorems in the Presence of seq
The paper is available via the ACM DL Author-ize feature:
| Authors: | P. Johann and J. Voigtländer |
|---|---|
| Published: | In 31st Symposium on Principles of Programming Languages (POPL'04, acceptance rate 29/176), Venice, Italy, Proceedings, volume 39(1) of SIGPLAN Notices, pages 99-110, ACM, January 2004. |
| DOI: | 10.1145/982962.964010 |
| BibTeX: | JV04.bib |
| 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. 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 forall-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 Girard-Reynolds-style calculus with fixpoints, algebraic datatypes, and seq. A crucial ingredient of our approach is the use of an asymmetric logical relation, which leads to "inequational" versions of free theorems enriched by preconditions guaranteeing their validity in the described setting. Besides the potential to obtain corresponding preconditions for standard equational free theorems by combining some new inequational ones, the latter also have value in their own right, as is exemplified with a careful analysis of seq's impact on familiar program transformations. |
| Download: | http://dl.acm.org/authorize?798512 (free) |
An extended version of this work appeared in Fundamenta Informaticae, see here.