[Haskell-cafe] Proving correctness

[Steffen Schuldenzucker]

On 02/11/2011 12:06 PM, C K Kashyap wrote:
> [...]
> I know that static typing and strong typing of Haskell eliminate a 
> whole class of problems - is that related to the proving correctness?
> [...]
You might have read about "free theorems" arising from types. They are a 
method to derive certain properties about a value that must hold, only 
looking at its type. For example, a value

 > x :: a

can't be anything else than bottom, a function

 > f :: [a] -> [a]

must commute with 'map', etc. For more information you may be interested 
in "Theorems for free"[1] by Philip Wadler.

[1] http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf