Free Theorems Involving Type Constructor Classes
The paper is available via the ACM DL Author-ize feature:
| 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. |