The 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). (Note there is also a third part to this correspondance, sometimes called the Curry-Howard-Lambek correspondance, that shows an equivalance to Cartesian closed categories)
1 The Answer
As is well established by now,
theAnswer :: Integer theAnswer = 42
2 InferenceA (non-trivial) Haskell function maps a value (of type
representation :: Bool -> Integer representation False = 0 representation True = 1
Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives and , though heavily disguised. Haskell handles conjuction in the manner described by Intuitionistic Logic. When a program has type , the value returned itself indicates which one. The algebraic data types in Haskell has a tag on each alternative, the constructor, to indicate the injections:
data Message a = OK a | Warning a | Error a p2pShare :: Integer -> Message String p2pShare n | n == 0 = Warning "Share! Freeloading hurts your peers." | n < 0 = Error "You cannot possibly share a negative number of files!" | n > 0 = OK ("You are sharing " ++ show n ++ " files."
show :: Message String -> String show (OK s) = s show (Warning s) = "Warning: " ++ s show (Error s) = "ERROR! " ++ s
The conjuction is handled via an isomorphism in Closed Cartesian Categories in general (Haskell types belong to this category): .
4 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)