Parametricity for Haskell with Imprecise Error Semantics

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

• Type: Conference
• Year: 2009
• Where: TLCA
• Authors: Florian Stenger, Janis Voigtländer
• Keywords: Glasgow Haskell Compiler, Polymorphic Function Types, Reasoning, Theoretical Computer Science, TLCA 2009