m (Curry-Howard isomorphism moved to Curry-Howard-Lambek correspondence)
Revision as of 05:45, 5 November 2006
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): . That is, instead of a function from to Z, we can have a function that takes an argument of type X and returns another function of type , that is, a function that takes Y to give (finally) a result of type Z: this technique is (known as currying) logically means .
(insert quasi-funny example here)
So in Haskell, currying takes care of the connective. Logically, a proof of is a pair (a,b) of proofs of the propositions. In Haskell, to have the final C value, values of both A and B have to be supplied (in turn) to the (curried) function.
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)
5 Type Classes
A type class in Haskell is a proposition about a type.
class Eq a where (==) :: a -> a -> Bool (/=) :: a -> a -> Bool
instance Eq Bool where True == True = True False == False = True _ == _ = False (/=) a b = not (a == b)
6 Indexed Types
(please someone complete this, should be quite interesting, I have no idea what it should look like logically)