# Curry-Howard-Lambek correspondence

### From HaskellWiki

BrettGiles (Talk | contribs) (Adding Lambek, categorization) |
Uchchwhash (Talk | contribs) |
||

Line 19: | Line 19: | ||

== Connectives == |
== 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. |
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 which one. The algebraic data types in Haskell has a tag on each alternative, the constructor, to indicate the injections: |
+ | 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 |
<haskell>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: | ||

</haskell> |
</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>. |
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>. |
||

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

+ | |||

+ | ''(insert quasi-funny example here)'' |
||

+ | |||

+ | So in Haskell, currying takes care of the <math>\and</math> connective. Logically, a proof of <math>A \and B</math> is a pair <math>(a, b)</math> of proofs of the propositions. In Haskell, to have the final <math>C</math> value, values of both <math>A</math> and <math>B</math> 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)</haskell> |
(.) f g x = f (g x)</haskell> |
||

The type is, actually, <hask>forall a b c. (a -> b) -> (b -> c) -> (a -> c)</hask>, to be a bit verbose, which says, logically speaking, for all propositions <hask>a, b</hask> and <hask>c</hask>, if from <hask>a</hask>, <hask>b</hask> can be proven, and if from <hask>b</hask>, <hask>c</hask> can be proven, then from <hask>a</hask>, <hask>c</hask> can be proven (the program says how to go about proving: just compose the given proofs!) |
The type is, actually, <hask>forall a b c. (a -> b) -> (b -> c) -> (a -> c)</hask>, to be a bit verbose, which says, logically speaking, for all propositions <hask>a, b</hask> and <hask>c</hask>, if from <hask>a</hask>, <hask>b</hask> can be proven, and if from <hask>b</hask>, <hask>c</hask> can be proven, then from <hask>a</hask>, <hask>c</hask> 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. |
||

+ | <haskell>class Eq a where |
||

+ | (==) :: a -> a -> Bool |
||

+ | (/=) :: a -> a -> Bool</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>). |
||

+ | 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: |
||

+ | <haskell>instance Eq Bool where |
||

+ | True == True = True |
||

+ | False == False = True |
||

+ | _ == _ = False |
||

+ | |||

+ | (/=) a b = not (a == b)</haskell> |
||

+ | |||

+ | == 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 |

## 1 The Answer

As is well established by now,

theAnswer :: Integer theAnswer = 42

*proves*the proposition

## 2 Inference

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

*constructs*a value of type

*transformed*into a proof of

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

## 3 Connectives

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

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