# Curry-Howard-Lambek correspondence

### From HaskellWiki

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

Line 10: | Line 10: | ||

== Inference == | == Inference == | ||

− | A (non-trivial) Haskell function | + | A (non-trivial) Haskell function 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 is ''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> | + | <haskell>representation :: Bool -> Integer |

− | + | representation False = 0 | |

− | + | representation 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). | says, for example, if <hask>Boolean</hask> is inhibited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery). | ||

== Connectives == | == Connectives == | ||

Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives <math>\and</math> and <math>\or</math>, though heavily disguised. | Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives <math>\and</math> and <math>\or</math>, though heavily disguised. | ||

− | Haskell handles <math>\or</math> conjuction in the manner described by Intuitionistic Logic. When a program has type <math>a \or b</math>, the value returned itself indicates | + | Haskell handles <math>\or</math> conjuction in the manner described by Intuitionistic Logic. When a program has type <math>a \or b</math>, 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: |

+ | <haskell>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." | ||

+ | </haskell> | ||

+ | So any one of <hask>OK String</hask>, <hask>Warning String</hask> or <hask>Error String</hask> proves the proposition <hask>Message String</hask>, leaving out any two constructors would not invalidate the program. At the same time, a proof of <hask>Message String</hask> can be pattern matched against the constructors to see which one it proves. | ||

+ | On the other hand, to prove <hask>String</hask> is inhibited from the proposition <hask>Message String</hask>, it has to be proven that you can prove <hask>String</hask> from any of the alternatives... | ||

+ | <haskell> | ||

+ | show :: Message String -> String | ||

+ | show (OK s) = s | ||

+ | show (Warning s) = "Warning: " ++ s | ||

+ | show (Error s) = "ERROR! " ++ s | ||

+ | </haskell> | ||

+ | The <math>\and</math> conjuction is handled via an isomorphism in Closed Cartesian Categories in general (Haskell types belong to this category): <math>\mathrm{Hom}(X\times Y,Z) \cong \mathrm{Hom}(X,Z^Y)</math>. | ||

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

## Revision as of 06:56, 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

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