[<<][compsci][>>][..]

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
laws).
[1] http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps

[Reply][About]

[<<][compsci][>>][..]