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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Johann, P., Voigtländer, J.: Free theorems in the presence of seq. In: POPL, Proceedings, pp. 99–110. ACM Press, New York (2004)
Johann, P., Voigtländer, J.: A family of syntactic logical relations for the semantics of Haskell-like languages. Information and Computation 207(2), 341–368 (2009)
Moran, A., Lassen, S.B., Peyton Jones, S.L.: Imprecise exceptions, Co-inductively. In: HOOTS, Proceedings. ENTCS, vol. 26, pp. 122–141. Elsevier, Amsterdam (1999)
Peyton Jones, S.L.: Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Proceedings of Marktoberdorf Summer School 2000, pp. 47–96. IOS Press, Amsterdam (2001)
Peyton Jones, S.L., Reid, A., Hoare, C.A.R., Marlow, S., Henderson, F.: A semantics for imprecise exceptions. In: PLDI, Proceedings, pp. 25–36. ACM Press, New York (1999)
Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3), 321–359 (2000)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing, Proceedings, pp. 513–523. Elsevier, Amsterdam (1983)
Stenger, F., Voigtländer, J.: Parametricity for Haskell with imprecise error semantics. Technical Report TUD-FI08-08, Technische Universität Dresden (2008)
Wadler, P.: Theorems for free. In: FPCA, Proceedings, pp. 347–359. ACM Press, New York (1989)
Xu, D.N., Peyton Jones, S.L., Claessen, K.: Static contract checking for Haskell. In: POPL, Proceedings, pp. 41–52. ACM Press, New York (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stenger, F., Voigtländer, J. (2009). Parametricity for Haskell with Imprecise Error Semantics. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)