Parametricity for Haskell with Imprecise Error Semantics
| Authors: | F. Stenger and J. Voigtländer |
|---|---|
| Published: | Technical Report TUD-FI08-08, Technische Universität Dresden, November 2008. |
| BibTeX: | SV08.bib |
| Abstract: | Types play an important role both in reasoning about Haskell and for its implementation. For example, the Glasgow Haskell Compiler performs certain fusion transformations that are intended to improve program efficiency and whose semantic justification is derived from polymorphic function types. At the same time, GHC adopts a scheme of error raising, propagation, and handling which is nondeterministic in the sense that there is some freedom as to which of a number of potential failure events hidden somewhere in a program is actually triggered. Implemented for good pragmatic reasons, this scheme complicates the meaning of programs and thus necessitates extra care when reasoning about them. In particular, since every erroneous value now represents a whole set of potential (but not arbitrary) failure causes, and since the associated propagation rules are askew to standard notions of program flow and value dependence, some standard laws suddenly fail to hold. This includes laws derived from polymorphic types, popularized as free theorems and at the base of the mentioned kind of fusion. We study this interaction between type-based reasoning and imprecise errors by revising and extending the foundational notion of relational parametricity, as well as further material required to make it applicable. More generally, we believe that our development and proofs help direct the way for incorporating further and other extensions and semantic features that deviate from the "naive" setting in which reasoning about Haskell programs often takes place. |
| Download: | ParametricityForHaskellWithImpreciseErrorSemantics_TR.pdf |
An abridged version of this work appeared at TLCA'09, see here.