Sun Sep 20 20:07:47 CEST 2009

Theorems for free!

Wadler's free theorems[1] and the algebra of programs.

A remark that caught my attention: ``in general the laws derived from
types are of a form useful for algebraic manipulation''. (I.e. push
`map' through a function).

These theorems depend on _parametricity_ : because of the _hole_ in
the specification, it can't do much else than be about _structure_.
The theorems then reflect structural theorems (i.e.  commutation

[1] http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps