| 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. |