Free Theorems Involving Type Constructor Classes

The paper is available via the ACM DL Author-ize feature:

ACM DL Author-ize service Free Theorems Involving Type Constructor Classes

Author: J. Voigtländer
Published: In 14th International Conference on Functional Programming (ICFP'09, acceptance rate 32/101), Edinburgh, Scotland, Proceedings, volume 44(9) of SIGPLAN Notices, pages 173-184, ACM, September 2009.
DOI: 10.1145/1596550.1596577
BibTeX: Voi09b.bib
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.
Download: http://dl.acm.org/authorize?139015 (free)
Slides: Slides of my talk at the conference are here.
Video: A video of the conference presentation is available here.