# Curry-Howard-Lambek correspondence

### From HaskellWiki

(Difference between revisions)

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 |

## 1 The Answer

As is well established by now,

theAnswer :: Integer theAnswer = 42

Integer

42

*proves*the proposition

Integer

## 2 Inference

A (non-trivial) Haskell function takes maps a value (of typea

b

*given*a value of type

a

a

*constructs*a value of type

b

*transformed*into a proof of

b

b

a

a -> b

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

Boolean

Integer

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

forall a b c. (a -> b) -> (b -> c) -> (a -> c)

a, b

c

a

b

b

c

a

c