# Curry-Howard-Lambek correspondence

### From HaskellWiki

BrettGiles (Talk | contribs) m (Curry-Howard Isomorphism moved to Curry-Howard isomorphism) |
BrettGiles (Talk | contribs) (Adding Lambek, categorization) |
||

Line 1: | Line 1: | ||

− | '''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''). |
+ | [[Category:Theoretical foundations]] |

+ | The '''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''). (Note there is also a third part to this correspondance, sometimes called the '''Curry-Howard-Lambek''' correspondance, that shows an equivalance to Cartesian closed [[Category theory|categories]]) |
||

__TOC__ |
__TOC__ |

## Revision as of 19:31, 2 November 2006

The **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*). (Note there is also a third part to this correspondance, sometimes called the **Curry-Howard-Lambek** correspondance, that shows an equivalance to Cartesian closed categories)

## Contents |

## 1 The Answer

As is well established by now,

theAnswer :: Integer theAnswer = 42

*proves*the proposition

## 2 Inference

A (non-trivial) Haskell function maps a value (of type*given*a value of type

*constructs*a value of type

*transformed*into a proof of

representation :: Bool -> Integer representation False = 0 representation True = 1

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

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

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