m (Curry-Howard Isomorphism moved to Curry-Howard isomorphism)
Revision as of 19:26, 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 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)