Curry-Howard-Lambek correspondence

From HaskellWiki

(Difference between revisions)

Revision as of 06:56, 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
2 Inference
3 Connectives
4 Theorems for free!

1 The Answer

As is well established by now,

theAnswer :: Integer
theAnswer = 42

The logical interpretation of the program is that the type

Integer

is inhibited (by the value

42

), so the existence of this program proves the proposition

Integer

(a type without any value is the "bottom" type, a proposition with no proof).

2 Inference

A (non-trivial) Haskell function maps a value (of type

a

, say) to another value (of type

b

), therefore, given a value of type

a

(a proof of

a

), it constructs a value of type

b

(so the proof is transformed into a proof of

b

)! So

b

is inhibited if

a

is, and a proof of

a -> b

is established (hence the notation, in case you were wondering).

representation :: Bool -> Integer
representation False = 0
representation True = 1

says, for example, if

Boolean

is inhibited, so is

Integer

(well, the point here is demonstration, not discovery).

3 Connectives

Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives $\and$ and $\or$ , though heavily disguised. Haskell handles $\or$ conjuction in the manner described by Intuitionistic Logic. When a program has type $a \or b$ , 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."

So any one of

OK String

Warning String

Error String

proves the proposition

Message String

, leaving out any two constructors would not invalidate the program. At the same time, a proof of

Message String

can be pattern matched against the constructors to see which one it proves. On the other hand, to prove

String

is inhibited from the proposition

Message String

, it has to be proven that you can prove

String

from any of the alternatives...

show :: Message String -> String
show (OK s) = s
show (Warning s) = "Warning: " ++ s
show (Error s) = "ERROR! " ++ s

The $\and$ conjuction is handled via an isomorphism in Closed Cartesian Categories in general (Haskell types belong to this category): $\mathrm{Hom}(X\times Y,Z) \cong \mathrm{Hom}(X,Z^Y)$ .

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)

The type is, actually,

forall a b c. (a -> b) -> (b -> c) -> (a -> c)

, to be a bit verbose, which says, logically speaking, for all propositions

a, b

and

c

, if from

a

b

can be proven, and if from

b

c

can be proven, then from

a

c

can be proven (the program says how to go about proving: just compose the given proofs!)

Retrieved from "http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence"

@@ Line 10: / Line 10: @@
 == Inference ==
-A (non-trivial) Haskell function takes maps a value (of type <hask>a</hask>, say) to another value (of type <hask>b</hask>), therefore, ''given'' a value of type <hask>a</hask> (a proof of <hask>a</hask>), it ''constructs'' a value of type <hask>b</hask> (so the proof its ''transformed'' into a proof of <hask>b</hask>)! So <hask>b</hask> is inhibited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering).
+A (non-trivial) Haskell function maps a value (of type <hask>a</hask>, say) to another value (of type <hask>b</hask>), therefore, ''given'' a value of type <hask>a</hask> (a proof of <hask>a</hask>), it ''constructs'' a value of type <hask>b</hask> (so the proof is ''transformed'' into a proof of <hask>b</hask>)! So <hask>b</hask> is inhibited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering).
-<haskell>toInteger :: Boolean -> Integer
+<haskell>representation :: Bool -> Integer
-inZ_2 False = 0
+representation False = 0
-inZ_2 True = 1</haskell>
+representation True = 1</haskell>
 says, for example, if <hask>Boolean</hask> is inhibited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery).
 == Connectives ==
 Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives <math>\and</math> and <math>\or</math>, though heavily disguised.
-Haskell handles <math>\or</math> conjuction in the manner described by Intuitionistic Logic. When a program has type <math>a \or b</math>, the value returned itself indicates its type.
+Haskell handles <math>\or</math> conjuction in the manner described by Intuitionistic Logic. When a program has type <math>a \or b</math>, 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:
+<haskell>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."
+</haskell>
+So any one of <hask>OK String</hask>, <hask>Warning String</hask> or <hask>Error String</hask> proves the proposition <hask>Message String</hask>, leaving out any two constructors would not invalidate the program. At the same time, a proof of <hask>Message String</hask> can be pattern matched against the constructors to see which one it proves.
+On the other hand, to prove <hask>String</hask> is inhibited from the proposition <hask>Message String</hask>, it has to be proven that you can prove <hask>String</hask> from any of the alternatives...
+<haskell>
+show :: Message String -> String
+show (OK s) = s
+show (Warning s) = "Warning: " ++ s
+show (Error s) = "ERROR! " ++ s
+</haskell>
+The <math>\and</math> conjuction is handled via an isomorphism in Closed Cartesian Categories in general (Haskell types belong to this category): <math>\mathrm{Hom}(X\times Y,Z) \cong \mathrm{Hom}(X,Z^Y)</math>.
 == Theorems for free! ==

Personal tools

Views