Parametricity for Haskell with Imprecise Error Semantics

Authors: F. Stenger and J. Voigtländer
Published: In 9th International Conference on Typed Lambda Calculi and Applications (TLCA'09, acceptance rate 27/53), Brasília, Brazil, Proceedings, volume 5608 of LNCS, pages 294-308, Springer, July 2009.
DOI: 10.1007/978-3-642-02273-9_22
BibTeX: SV09a.bib
Abstract: Error raising, propagation, and handling in Haskell can be imprecise in the sense that a language implementation's choice of local evaluation order, and optimizing transformations to apply, may influence which of a number of potential failure events hidden somewhere in a program is actually triggered. While this has pragmatic advantages from an implementation point of view, it also complicates the meaning of programs and thus requires extra care when reasoning about them. The proper semantic setup is one in which every erroneous value represents a whole set of potential (but not arbitrary) failure causes. The associated propagation rules are somewhat askew to standard notions of program flow and value dependence. As a consequence, standard reasoning techniques are cast into doubt, and rightly so. We study this issue in depth for one such reasoning technique, namely the derivation of free theorems from polymorphic types. We revise and extend the foundational notion of relational parametricity, as well as further material required to make it applicable.
Download: ParametricityForHaskellWithImpreciseErrorSemantics.pdf
Rights: Copyright held by Springer.
Slides: Slides of my talk at the conference are here.