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.
According to [Str67], parametric polymorphic functions behave uniformly at every type. In functional programming languages based on the polymorphic lambda calculus of Girard and Reynolds [Gir72, Rey74], this concept is captured by parametricity theorems [Rey83, Wad89]. In [Wad89], it was then pointed out how these theorems may be used to derive properties of functions, especially of parametric polymorphic ones, solely from the their types, that is, virtually for free. This is the reason why the results obtained from parametricity theorems are also called free theorems.
The key idea of [Rey83], which finally leads to free theorems, is to interpret types as relations instead of as sets. In this setting, type variables are interpreted as relations, basic types are usually interpreted as identity relations and, for every type constructor of arity n, there is a relational action which maps n given relations to a relational interpretation of the type constructor. In particular, there are relational actions for the type constructor of function types and for type abstractions, but in the same way, also relational actions for (selected) user-defined data type may be defined. Based on these relational actions, a logical relation [Plo80, Sta85] may be constructed, for which a parametricity theorem can then be proven. Note that the whole process is basically a rewriting of types into relational interpretations and finally into free theorems, which can also be automated.
Current functional programming languages like Haskell [Jon03] feature language constructs not available in the Girard-Reynolds calculus, notably undefined values, fixpoint combinators and selective strictness. Several works [JV06, LP96, Wad89] have studied the impact of these extensions on free theorems and found out suitable restrictions such that similar, but weaker free theorems can still be obtained.
- 2.1 User-defined data types
2.2 Type classes
- 3.1 Preliminaries
3.2 Type expressions
3.3 Type constructors and type classes
3.4 Semantics of closed type expressions
3.5 Relational actions
3.6 Logical relations
3.7 Parametricity theorems
4 Free theorems
- 4.1 The basic model
4.2 The fix models
4.3 The seq models
4.4 Type classes
- 5.1 The library free-theorems
5.2 The user interface ftshell
5.3 Used applications and libraries