# Curry-Howard-Lambek correspondence

(Difference between revisions)
 Revision as of 19:31, 2 November 2006 (edit) (Adding Lambek, categorization)← Previous diff Revision as of 15:08, 4 November 2006 (edit) (undo)Next diff → Line 19: Line 19: == Connectives == == Connectives == Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives $\and$ and $\or$, though heavily disguised. 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: + 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 data Message a = OK a | Warning a | Error a + p2pShare :: Integer -> Message String p2pShare :: Integer -> Message String p2pShare n | n == 0 = Warning "Share! Freeloading hurts your peers." p2pShare n | n == 0 = Warning "Share! Freeloading hurts your peers." Line 35: Line 36: 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)$. 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. == Theorems for free! == == Theorems for free! == Line 41: Line 47: (.) f g x = f (g x) (.) 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!) 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!) + + == 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 inhibited, 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) + + == Indexed Types == + ''(please someone complete this, should be quite interesting, I have no idea what it should look like logically)''

## Revision as of 15:08, 4 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)

## Contents

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
| 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
or
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)$. 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.

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

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 inhibited, 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)

## 6 Indexed Types

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