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

Uchchwhash (talk | contribs) (starting a semi-project, need help! (especially for Indexed Types)) |
Uchchwhash (talk | contribs) (oops) |
||

Line 5: | Line 5: | ||

== The Answer == |
== The Answer == |
||

As is well established by now, |
As is well established by now, |
||

− | |||

− | |||

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

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

⚫ | |||

⚫ | |||

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

+ | Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem. |
||

+ | <haskell>(.) :: (a -> b) -> (b -> c) -> (a -> c) |
||

+ | (.) 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!) |

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

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