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

Uchchwhash (talk | contribs) (oops) |
Uchchwhash (talk | contribs) |
||

Line 8: | Line 8: | ||

theAnswer = 42</haskell> |
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 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). |
||

+ | |||

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

+ | <haskell>toInteger :: Boolean -> Integer |
||

+ | toInteger False = 0 |
||

+ | toInteger 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). |
||

== Theorems for free! == |
== Theorems for free! == |

## Revision as of 03:32, 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*).

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

## Inference

A (non-trivial) Haskell function takes 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 its *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).

```
toInteger :: Boolean -> Integer
toInteger False = 0
toInteger True = 1
```

says, for example, if `Boolean`

is inhibited, so is `Integer`

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

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