Sun Sep 20 20:07:47 CEST 2009
Theorems for free!
Wadler's free theorems 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