| Authors: |
P. Johann and J. Voigtländer |
| Published: |
Fundamenta Informaticae, volume 69(1-2), pages 63-102, IOS Press, 2006. |
| BibTeX: |
JV06.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, standard parametricity results - including so-called
free theorems - fail for nonstrict languages supporting a polymorphic
strict evaluation primitive such as Haskell's seq. A folk theorem
maintains that such results hold for a subset of Haskell corresponding
to a Girard-Reynolds calculus with fixpoints and algebraic datatypes
even when seq is present provided the relations which appear
in their derivations are required to be bottom-reflecting and
admissible. In this paper we show that this folklore is incorrect, but
that parametricity results can be recovered in the presence of
seq by restricting attention to left-closed, total, and admissible
relations instead. The key novelty of our approach is the asymmetry
introduced by left-closedness, which leads to "inequational" versions
of standard parametricity results together with preconditions
guaranteeing their validity even when seq is present. We use these
results to derive criteria ensuring that both equational and
inequational versions of short cut fusion and related program
transformations based on free theorems hold in the presence of seq.
|
| Download: |
TheImpactOfSeqOnFreeTheoremsBasedProgramTransformations.pdf |
| Rights: |
Copyright held by the authors. Exclusive publishing license granted to IOS Press. |
| Slides: |
Slides of a talk I gave about this paper are here. |