# Curry-Howard-Lambek correspondence

### From HaskellWiki

(Difference between revisions)

Uchchwhash (Talk | contribs) |
Uchchwhash (Talk | contribs) (more to come) |

## Revision as of 04:16, 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 inZ_2 False = 0 inZ_2 True = 1

Boolean

Integer

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

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

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

a, b

c

a

b

b

c

a

c