[Haskell-cafe] Proving correctness
sschuldenzucker at uni-bonn.de
Fri Feb 11 13:17:34 CET 2011
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" by Philip Wadler.
More information about the Haskell-Cafe