Parametricity for Haskell with Imprecise Error Semantics Export

@inproceedings{SV09a, 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.}, author = {Stenger, Florian and Voigtl\"{a}nder, Janis}, booktitle = {Typed Lambda Calculi and Applications, Proceedings}, citeulike-article-id = {5202216}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-02273-9_22}, citeulike-linkout-1 = {http://www.springerlink.com/content/88763x4404664771}, citeulike-linkout-2 = {http://wwwtcs.inf.tu-dresden.de/~voigt/tlca09.pdf}, doi = {10.1007/978-3-642-02273-9_22}, editor = {Curien, Pierre-Louis}, journal = {Typed Lambda Calculi and Applications}, keywords = {denotational-semantics, exceptions, free-theorems, functional-programming, haskell, imprecise-errors, lambda-calculus, lazy-evaluation, logical-relations, nondeterminism, parametricity, polymorphism, selective-strictness, seq, types}, month = {July}, pages = {294--308}, posted-at = {2009-07-19 07:22:37}, priority = {0}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, title = {Parametricity for Haskell with Imprecise Error Semantics}, url = {http://dx.doi.org/10.1007/978-3-642-02273-9_22}, volume = {5608}, year = {2009} }

TY - CONF ID - SV09a L3 - citeulike-article-id:5202216 N2 - 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. JF - Typed Lambda Calculi and Applications SE - Lecture Notes in Computer Science EP - 308 TI - Parametricity for Haskell with Imprecise Error Semantics PB - Springer-Verlag VL - 5608 T2 - Typed Lambda Calculi and Applications, Proceedings SP - 294 KW - denotational-semantics KW - exceptions KW - free-theorems KW - functional-programming KW - haskell KW - imprecise-errors KW - lambda-calculus KW - lazy-evaluation KW - logical-relations KW - nondeterminism KW - parametricity KW - polymorphism KW - selective-strictness KW - seq KW - types AU - Stenger, Florian AU - Voigtländer, Janis A2 - Curien, Pierre-Louis PY - 2009/07// UR - http://dx.doi.org/10.1007/978-3-642-02273-9_22 ER -