Curry-Howard-Lambek correspondence
From HaskellWiki
BrettGiles (Talk | contribs) (Adding Lambek, categorization) |
m |
||
(15 intermediate revisions by 7 users not shown) | |||
Line 1: | Line 1: | ||
[[Category:Theoretical foundations]] | [[Category:Theoretical foundations]] | ||
− | The '''Curry-Howard | + | |
+ | {{Foundations infobox}} | ||
+ | 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__ | ||
− | == | + | == Life, the Universe and Everything == |
As is well established by now, | As is well established by now, | ||
<haskell>theAnswer :: Integer | <haskell>theAnswer :: Integer | ||
theAnswer = 42</haskell> | theAnswer = 42</haskell> | ||
− | The logical interpretation of the program is that the type <hask>Integer</hask> is | + | The logical interpretation of the program is that the type <hask>Integer</hask> is inhabited (by the value <hask>42</hask>), so the existence of this program ''proves'' the proposition <hask>Integer</hask> (a type without any value is the "bottom" type, a proposition with no proof). |
== Inference == | == Inference == | ||
− | 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 | + | 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 inhabited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering). |
− | <haskell>representation :: Bool -> Integer | + | |
+ | <haskell> | ||
+ | representation :: Bool -> Integer | ||
representation False = 0 | representation False = 0 | ||
− | representation True = 1</haskell> | + | representation True = 1 |
− | says, for example, if <hask>Boolean</hask> is | + | </haskell> |
+ | |||
+ | says, for example, if <hask>Boolean</hask> is inhabited, 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> | + | 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 | <haskell>data Message a = OK a | Warning a | Error a | ||
+ | |||
p2pShare :: Integer -> Message String | p2pShare :: Integer -> Message String | ||
p2pShare n | n == 0 = Warning "Share! Freeloading hurts your peers." | p2pShare n | n == 0 = Warning "Share! Freeloading hurts your peers." | ||
| n < 0 = Error "You cannot possibly share a negative number of files!" | | n < 0 = Error "You cannot possibly share a negative number of files!" | ||
− | | n > 0 = OK ("You are sharing " ++ show n ++ " files." | + | | n > 0 = OK ("You are sharing " ++ show n ++ " files.") |
</haskell> | </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. | 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 | + | On the other hand, to prove <hask>String</hask> is inhabited 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> | <haskell> | ||
show :: Message String -> String | show :: Message String -> String | ||
Line 35: | Line 42: | ||
</haskell> | </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>. | 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>. | ||
+ | That is, instead of a function from <math>X \times Y</math> to <math>Z</math>, we can have a function that takes an argument of type <math>X</math> and returns another function of type <math>Y \rightarrow Z</math>, that is, a function that takes <math>Y</math> to give (finally) a result of type <math>Z</math>: this technique is (known as currying) logically means <math>A \and B \rightarrow C \iff A \rightarrow (B \rightarrow C)</math>. | ||
+ | |||
+ | ''(insert quasi-funny example here)'' | ||
+ | |||
+ | So in Haskell, currying takes care of the <math>\and</math> connective. Logically, a proof of <math>A \and B</math> is a pair <math>(a, b)</math> of proofs of the propositions. In Haskell, to have the final <math>C</math> value, values of both <math>A</math> and <math>B</math> have to be supplied (in turn) to the (curried) function. | ||
== Theorems for free! == | == Theorems for free! == | ||
Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem. | Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem. | ||
− | <haskell>(.) :: (a -> b) -> (b -> c) -> (a -> c) | + | |
− | (.) f g x = f (g x)</haskell> | + | <haskell> |
+ | (.) :: (a -> b) -> (b -> c) -> (a -> c) | ||
+ | (.) f g x = f (g x) | ||
+ | </haskell> | ||
+ | |||
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!) | ||
+ | |||
+ | == Negation == | ||
+ | Of course, there's not much you can do with just truth. <hask>forall b. a -> b</hask> says that given <hask>a</hask>, we can infer anything. Therefore we will take <hask>forall b. a -> b</hask> as meaning <hask>not a</hask>. Given this, we can prove several more of the axioms of logic. | ||
+ | |||
+ | <haskell> | ||
+ | type Not x = (forall a. x -> a) | ||
+ | |||
+ | doubleNegation :: x -> Not (Not x) | ||
+ | doubleNegation k pr = pr k | ||
+ | |||
+ | contraPositive :: (a -> b) -> (Not b -> Not a) | ||
+ | contraPositive fun denyb showa = denyb (fun showa) | ||
+ | |||
+ | deMorganI :: (Not a, Not b) -> Not (Either a b) | ||
+ | deMorganI (na, _) (Left a) = na a | ||
+ | deMorganI (_, nb) (Right b) = nb b | ||
+ | |||
+ | deMorganII :: Either (Not a) (Not b) -> Not (a,b) | ||
+ | deMorganII (Left na) (a, _) = na a | ||
+ | deMorganII (Right nb) (_, b) = nb b | ||
+ | </haskell> | ||
+ | |||
+ | == Type classes == | ||
+ | A type class in Haskell is a proposition ''about'' a [[type]]. | ||
+ | |||
+ | <haskell> | ||
+ | class Eq a where | ||
+ | (==) :: a -> a -> Bool | ||
+ | (/=) :: a -> a -> Bool | ||
+ | </haskell> | ||
+ | |||
+ | means, logically, there is a type <hask>a</hask> for which the type <hask>a -> a -> Bool</hask> is inhabited, or, from <hask>a</hask> it can be proved that <hask>a -> a -> Bool</hask> (the class promises two different proofs for this, having names <hask>==</hask> and <hask>/=</hask>). | ||
+ | This proposition is of existential nature (not to be confused with [[existential type]]). A proof for this proposition (that there is a type that conforms to the specification) is (obviously) a set of proofs of the advertised proposition (an implementation), by an <hask>instance</hask> | ||
+ | declaration: | ||
+ | |||
+ | <haskell> | ||
+ | instance Eq Bool where | ||
+ | True == True = True | ||
+ | False == False = True | ||
+ | _ == _ = False | ||
+ | |||
+ | (/=) a b = not (a == b) | ||
+ | </haskell> | ||
+ | |||
+ | A not-so-efficient sort implementation would be: | ||
+ | |||
+ | <haskell> | ||
+ | sort [] = [] | ||
+ | sort (x : xs) = sort lower ++ [x] ++ sort higher | ||
+ | where (lower,higher) = partition (< x) xs | ||
+ | </haskell> | ||
+ | |||
+ | 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>sort</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 constitute a Prolog-like logic language, and multiparameter type classes define a relation between types. | ||
+ | === [[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. | ||
+ | |||
+ | == Indexed types == | ||
+ | ''(please someone complete this, should be quite interesting, I have no idea what it should look like logically)'' |
Latest revision as of 21:35, 21 February 2010
Haskell theoretical foundations
General: Lambda calculus: Other: |
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 |
[edit] 1 Life, the Universe and Everything
As is well established by now,
theAnswer :: Integer theAnswer = 42
[edit] 2 Inference
A (non-trivial) Haskell function maps a value (of typerepresentation :: Bool -> Integer representation False = 0 representation True = 1
[edit] 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.
[edit] 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)
[edit] 5 Negation
Of course, there's not much you can do with just truth.type Not x = (forall a. x -> a) doubleNegation :: x -> Not (Not x) doubleNegation k pr = pr k contraPositive :: (a -> b) -> (Not b -> Not a) contraPositive fun denyb showa = denyb (fun showa) deMorganI :: (Not a, Not b) -> Not (Either a b) deMorganI (na, _) (Left a) = na a deMorganI (_, nb) (Right b) = nb b deMorganII :: Either (Not a) (Not b) -> Not (a,b) deMorganII (Left na) (a, _) = na a deMorganII (Right nb) (_, b) = nb b
[edit] 6 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 sort implementation would be:
sort [] = [] sort (x : xs) = sort lower ++ [x] ++ sort higher where (lower,higher) = partition (< x) xs
[edit] 7 Multi-parameter type classes
Haskell makes frequent use of multiparameter type classes. Type classes constitute a Prolog-like logic language, and multiparameter type classes define a relation between types.
[edit] 7.1 Functional dependencies
These type level functions are set-theoretic. That is,[edit] 8 Indexed types
(please someone complete this, should be quite interesting, I have no idea what it should look like logically)