# 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 | + | 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 | + | == 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. | ||

− | == | + | == 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 | + | === [[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 | + | == 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)*