# Curry-Howard-Lambek correspondence

### From HaskellWiki

Uchchwhash (Talk | contribs) m (fmt, accidentally overwrote dons' fmts) |
BrettGiles (Talk | contribs) (Revise intro to be more descriptive of three way correspondance; links) |
||

Line 1: | Line 1: | ||

[[Category:Theoretical foundations]] |
[[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''). There is also a third part, sometimes called the '''Curry-Howard-Lambek''' correspondance, that shows an equivalance to Cartesian closed [[Category theory|categories]]. |
+ | The '''Curry-Howard-Lambek correspondance''' is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed [[Category theory|category]]. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and ''vice versa''). |

__TOC__ |
__TOC__ |
||

Line 56: | Line 56: | ||

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

− | == Type Classes == |
+ | == Type classes == |

A type class in Haskell is a proposition ''about'' a [[type]]. |
A type class in Haskell is a proposition ''about'' a [[type]]. |
||

Line 89: | Line 89: | ||

Haskell infers its type to be <hask>forall a. (Ord a) => [a] -> [a]</hask>. It means, if a type <hask>a</hask> satisfies the proposition about propositions <hask>Ord</hask> (that is, has an ordering defined, as is necessary for comparison), then <hask>quickSort</hask> is a proof of <hask>[a] -> [a]</hask>. For this to work, somewhere, it should be proved (that is, the comparison functions defined) that <hask>Ord a</hask> is true. |
Haskell infers its type to be <hask>forall a. (Ord a) => [a] -> [a]</hask>. It means, if a type <hask>a</hask> satisfies the proposition about propositions <hask>Ord</hask> (that is, has an ordering defined, as is necessary for comparison), then <hask>quickSort</hask> is a proof of <hask>[a] -> [a]</hask>. For this to work, somewhere, it should be proved (that is, the comparison functions defined) that <hask>Ord a</hask> is true. |
||

− | == Multiparameter Type Classes == |
+ | == Multi-parameter type classes == |

Haskell makes frequent use of multiparameter type classes. Type classes use a logic language (Prolog-like), and for multiparamter type classes they define a relation between types. |
Haskell makes frequent use of multiparameter type classes. Type classes use a logic language (Prolog-like), and for multiparamter type classes they define a relation between types. |
||

− | === Functional Dependencies === |
+ | === [[Functional dependencies]] === |

These type level functions are set-theoretic. That is, <hask> class TypeClass a b | a -> b</hask> defines a relation between types <hask>a</hask> and <hask>b</hask>, and requires that there would not be different instances of <hask>TypeClass a b</hask> and <hask>TypeClass a c</hask> for different <hask>b</hask> and <hask>c</hask>, so that, essentially, <hask>b</hask> can be inferred as soon as <hask>a</hask> is known. This is precisely functions as relations as prescribed by set theory. |
These type level functions are set-theoretic. That is, <hask> class TypeClass a b | a -> b</hask> defines a relation between types <hask>a</hask> and <hask>b</hask>, and requires that there would not be different instances of <hask>TypeClass a b</hask> and <hask>TypeClass a c</hask> for different <hask>b</hask> and <hask>c</hask>, so that, essentially, <hask>b</hask> can be inferred as soon as <hask>a</hask> is known. This is precisely functions as relations as prescribed by set theory. |
||

− | == Indexed Types == |
+ | == Indexed types == |

''(please someone complete this, should be quite interesting, I have no idea what it should look like logically)'' |
''(please someone complete this, should be quite interesting, I have no idea what it should look like logically)'' |

## Revision as of 20:59, 6 November 2006

The **Curry-Howard-Lambek correspondance** is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (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): .
That is, instead of a function from to *Z*, we can have a function that takes an argument of type *X* and returns another function of type , that is, a function that takes *Y* to give (finally) a result of type *Z*: this technique is (known as currying) logically means .

*(insert quasi-funny example here)*

So in Haskell, currying takes care of the connective. Logically, a proof of is a pair (*a*,*b*) of proofs of the propositions. In Haskell, to have the final *C* value, values of both *A* and *B* have to be supplied (in turn) to the (curried) function.

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

## 5 Type classes

A type class in Haskell is a proposition *about* a type.

class Eq a where (==) :: a -> a -> Bool (/=) :: a -> a -> Bool

declaration:

instance Eq Bool where True == True = True False == False = True _ == _ = False (/=) a b = not (a == b)

A not-so-efficient Quicksort implementation would be:

quickSort [] = [] quickSort (x : xs) = quickSort lower ++ [x] ++ quickSort higher where lower = filter (<= x) xs higher = filter (> x) xs

## 6 Multi-parameter type classes

Haskell makes frequent use of multiparameter type classes. Type classes use a logic language (Prolog-like), and for multiparamter type classes they define a relation between types.

### 6.1 Functional dependencies

These type level functions are set-theoretic. That is,## 7 Indexed types

*(please someone complete this, should be quite interesting, I have no idea what it should look like logically)*