# Difference between revisions of "Curry-Howard-Lambek correspondence"

BrettGiles (talk | contribs) (Revise intro to be more descriptive of three way correspondance; links) |
Uchchwhash (talk | contribs) m (inhibit -> inhabit) |
||

Line 8: | Line 8: | ||

<haskell>theAnswer :: Integer |
<haskell>theAnswer :: Integer |
||

theAnswer = 42</haskell> |
theAnswer = 42</haskell> |
||

− | The logical interpretation of the program is that the type <hask>Integer</hask> is |
+ | 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 == |
== 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 |
+ | 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> |
<haskell> |
||

Line 19: | Line 19: | ||

</haskell> |
</haskell> |
||

− | says, for example, if <hask>Boolean</hask> is |
+ | says, for example, if <hask>Boolean</hask> is inhabited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery). |

== Connectives == |
== Connectives == |
||

Line 32: | Line 32: | ||

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

show :: Message String -> String |
show :: Message String -> String |
||

Line 65: | Line 65: | ||

</haskell> |
</haskell> |
||

− | means, logically, there is a type <hask>a</hask> for which the type <hask>a -> a -> Bool</hask> is |
+ | 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> |
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: |
declaration: |

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

## Contents

## 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).

## 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).

## 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."
```

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 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 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 , we can have a function that takes an argument of type and returns another function of type , that is, a function that takes to give (finally) a result of type : 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 of proofs of the propositions. In Haskell, to have the final value, values of both and have to be supplied (in turn) to the (curried) function.

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

## 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.

## 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.

### 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.

## Indexed types

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