(starting a semi-project, need help! (especially for Indexed Types))
Revision as of 03:08, 2 November 2006
Curry-Howard Isomorphism is an isomorphism between types (in programming languages) and propositions (in logic). Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs (and vice versa).
1 The Answer
As is well established by now,
theAnswer :: Integer theAnswer = 42
2 Theorems for free!
Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem.
(.) :: (a -> b) -> (b -> c) -> (a -> c) (.) f g x = f (g x)