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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
