Free Theorems for Sublanguages of Haskell

Sascha Böhme

Document: PDF

Abstract: Pure functional programs fulfill properties which can be derived solely from the types of their functions, especially from types of parametric polymorphic functions. These properties are called parametricity results, or more commonly, free theorems. First only considered for the polymorphic lambda calculus of Girard and Reynolds, research has studied how adding aspects of current functional programming languages like Haskell influence the expressiveness of such free theorems. These aspects cover undefined values, fixpoint combinators and selective strictness. The contribution of this thesis is to subsume these results in one common scheme and to enhance it with other aspects of Haskell, namely simple type classes and three kinds of user-defined data types. Additionally, several simplifications commonly used in deriving free theorems are identified. Based on these theoretic foundations, an implementation is described which allows to automatically generate free theorems.

Bibtex entry:

  author = {Sascha B\"ohme},
  title = {Free Theorems for Sublanguages of Haskell},
  school = {Technische Universit\"at Dresden},
  year = 2007

Online: An extended version based on the work originally written as part of this thesis can be found at