Curry-Howard-Lambek correspondence

From HaskellWiki

(Difference between revisions)

Revision as of 13:48, 18 November 2006

The Curry-Howard-Lambek correspondance is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa).

1 The Answer
2 Inference
3 Connectives
4 Theorems for free!
5 Type classes
6 Multi-parameter type classes
- 6.1 Functional dependencies
7 Indexed types

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 inhabited (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 inhabited 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 inhabited, 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 inhabited 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)$ . That is, instead of a function from $X \times Y$ to $Z$ , we can have a function that takes an argument of type $X$ and returns another function of type $Y \rightarrow Z$ , that is, a function that takes $Y$ to give (finally) a result of type $Z$ : this technique is (known as currying) logically means $A \and B \rightarrow C \iff A \rightarrow (B \rightarrow C)$ .

(insert quasi-funny example here)

So in Haskell, currying takes care of the $\and$ connective. Logically, a proof of $A \and B$ 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)

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!)

5 Type classes

A type class in Haskell is a proposition about a type.

class Eq a where
    (==) :: a -> a -> Bool
    (/=) :: a -> a -> Bool

means, logically, there is a type

a

for which the type

a -> a -> Bool

is inhabited, or, from

a

it can be proved that

a -> a -> Bool

(the class promises two different proofs for this, having names

==

and

/=

). This proposition is of existential nature (not to be confused with existential type). A proof for this proposition (that there is a type that conforms to the specification) is (obviously) a set of proofs of the advertized proposition (an implementation), by an

instance

declaration:

instance Eq Bool where
    True  == True  = True
    False == False = True
    _     == _     = False
 
(/=) a b = not (a == b)

A not-so-efficient Quicksort implementation would be:

quickSort [] = []
quickSort (x : xs) = quickSort lower ++ [x] ++ quickSort higher
                     where lower = filter (<= x) xs
                           higher = filter (> x) xs

Haskell infers its type to be

forall a. (Ord a) => [a] -> [a]

. It means, if a type

a

satisfies the proposition about propositions

Ord

(that is, has an ordering defined, as is necessary for comparison), then

quickSort

is a proof of

[a] -> [a]

. For this to work, somewhere, it should be proved (that is, the comparison functions defined) that

Ord a

is true.

6 Multi-parameter type classes

Haskell makes frequent use of multiparameter type classes. Type classes use a logic language (Prolog-like), and for multiparamter type classes they define a relation between types.

6.1 Functional dependencies

These type level functions are set-theoretic. That is,

class TypeClass a b | a -> b

defines a relation between types

a

and

b

, and requires that there would not be different instances of

TypeClass a b

and

TypeClass a c

for different

b

and

c

, so that, essentially,

b

can be inferred as soon as

a

is known. This is precisely functions as relations as prescribed by set theory.

7 Indexed types

(please someone complete this, should be quite interesting, I have no idea what it should look like logically)

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

Category: Theoretical foundations

@@ Line 8: / Line 8: @@
 <haskell>theAnswer :: Integer
 theAnswer = 42</haskell>
-The logical interpretation of the program is that the type <hask>Integer</hask> is inhibited (by the value <hask>42</hask>), so the existence of this program ''proves'' the proposition <hask>Integer</hask> (a type without any value is the "bottom" type, a proposition with no proof).
+The logical interpretation of the program is that the type <hask>Integer</hask> is inhabited (by the value <hask>42</hask>), so the existence of this program ''proves'' the proposition <hask>Integer</hask> (a type without any value is the "bottom" type, a proposition with no proof).
 == Inference ==
-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).
+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 inhabited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering).
 <haskell>
@@ Line 19: / Line 19: @@
 </haskell>
-says, for example, if <hask>Boolean</hask> is inhibited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery).
+says, for example, if <hask>Boolean</hask> is inhabited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery).
 == Connectives ==
@@ Line 32: / Line 32: @@
 </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...
+On the other hand, to prove <hask>String</hask> is inhabited 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
@@ Line 65: / Line 65: @@
 </haskell>
-means, logically, there is a type <hask>a</hask> for which the type <hask>a -> a -> Bool</hask> is inhibited, or, from <hask>a</hask> it can be proved that <hask>a -> a -> Bool</hask> (the class promises two different proofs for this, having names <hask>==</hask> and <hask>/=</hask>).
+means, logically, there is a type <hask>a</hask> for which the type <hask>a -> a -> Bool</hask> is inhabited, or, from <hask>a</hask> it can be proved that <hask>a -> a -> Bool</hask> (the class promises two different proofs for this, having names <hask>==</hask> and <hask>/=</hask>).
 This proposition is of existential nature (not to be confused with [[existential type]]). A proof for this proposition (that there is a type that conforms to the specification) is (obviously) a set of proofs of the advertized proposition (an implementation), by an <hask>instance</hask>
 declaration:

Personal tools

Views