 |
Free Theorems Involving Type Constructor Classes
Janis Voigtlaender
The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)Edinburgh, Scotland, 31st August - 2nd September 2009
Abstract
Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type *constructors* restricted by *class constraints*. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof.
START Conference Manager (V2.56.8 - Rev. 748M)