Difference between revisions of "CurryHowardLambek correspondence"
Uchchwhash (talk  contribs) 
(Fixed Haskell definition of (.)) 

(18 intermediate revisions by 8 users not shown)  
Line 1:  Line 1:  
⚫  
+  [[Category:Theoretical foundations]] 

+  
+  {{Foundations infobox}} 

⚫  The '''CurryHowardLambek correspondance''' is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed [[Category theorycategory]]. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and ''vice versa''). 

__TOC__ 
__TOC__ 

−  == The Answer == 

+  == 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 (nontrivial) 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 (nontrivial) 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 

representation False = 0 
representation False = 0 

−  representation True = 1 
+  representation True = 1 
−  +  </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 34:  Line 38:  
</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 quasifunny 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) 

+  
−  +  <haskell> 

−  +  (.) :: (b > c) > (a > b) > (a > c) 

+  (.) f g x = f (g x) 

+  </haskell> 

+  
+  The type is, actually, <hask>forall a b c. (b > c) > (a > b) > (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 notsoefficient 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. 

+  
+  == Multiparameter type classes == 

+  Haskell makes frequent use of multiparameter type classes. Type classes constitute a Prologlike logic language, and multiparameter type classes define a relation between types. 

+  === [[Functional dependencies]] === 

+  These type level functions are settheoretic. 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 15:42, 18 November 2019
Haskell theoretical foundations
General: Lambda calculus: Other: 
The CurryHowardLambek 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
Life, the Universe and Everything
As is well established by now,
theAnswer :: Integer
theAnswer = 42
The logical interpretation of the program is that the type Integer
is inhabited (by the value 42
), so the existence of this program proves the proposition Integer
(a type without any value is the "bottom" type, a proposition with no proof).
Inference
A (nontrivial) Haskell function maps a value (of type a
, say) to another value (of type b
), therefore, given a value of type a
(a proof of a
), it constructs a value of type b
(so the proof is transformed into a proof of b
)! So b
is inhabited if a
is, and a proof of a > b
is established (hence the notation, in case you were wondering).
representation :: Bool > Integer
representation False = 0
representation True = 1
says, for example, if Boolean
is inhabited, so is Integer
(well, the point here is demonstration, not discovery).
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.")
So any one of OK String
, Warning String
or Error String
proves the proposition Message String
, leaving out any two constructors would not invalidate the program. At the same time, a proof of Message String
can be pattern matched against the constructors to see which one it proves.
On the other hand, to prove String
is inhabited from the proposition Message String
, it has to be proven that you can prove String
from any of the alternatives...
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 , we can have a function that takes an argument of type and returns another function of type , that is, a function that takes to give (finally) a result of type : this technique is (known as currying) logically means .
(insert quasifunny example here)
So in Haskell, currying takes care of the connective. Logically, a proof of is a pair of proofs of the propositions. In Haskell, to have the final value, values of both and have to be supplied (in turn) to the (curried) function.
Theorems for free!
Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem.
(.) :: (b > c) > (a > b) > (a > c)
(.) f g x = f (g x)
The type is, actually, forall a b c. (b > c) > (a > b) > (a > c)
, to be a bit verbose, which says, logically speaking, for all propositions a, b
and c
, if from a
, b
can be proven, and if from b
, c
can be proven, then from a
, c
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. forall b. a > b
says that given a
, we can infer anything. Therefore we will take forall b. a > b
as meaning not a
. Given this, we can prove several more of the axioms of logic.
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
Type classes
A type class in Haskell is a proposition about a type.
class Eq a where
(==) :: a > a > Bool
(/=) :: a > a > Bool
means, logically, there is a type a
for which the type a > a > Bool
is inhabited, or, from a
it can be proved that a > a > Bool
(the class promises two different proofs for this, having names ==
and /=
).
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 instance
declaration:
instance Eq Bool where
True == True = True
False == False = True
_ == _ = False
(/=) a b = not (a == b)
A notsoefficient sort implementation would be:
sort [] = []
sort (x : xs) = sort lower ++ [x] ++ sort higher
where (lower,higher) = partition (< x) xs
Haskell infers its type to be forall a. (Ord a) => [a] > [a]
. It means, if a type a
satisfies the proposition about propositions Ord
(that is, has an ordering defined, as is necessary for comparison), then sort
is a proof of [a] > [a]
. For this to work, somewhere, it should be proved (that is, the comparison functions defined) that Ord a
is true.
Multiparameter type classes
Haskell makes frequent use of multiparameter type classes. Type classes constitute a Prologlike logic language, and multiparameter type classes define a relation between types.
Functional dependencies
These type level functions are settheoretic. That is, class TypeClass a b  a > b
defines a relation between types a
and b
, and requires that there would not be different instances of TypeClass a b
and TypeClass a c
for different b
and c
, so that, essentially, b
can be inferred as soon as a
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)