Curry-Howard-Lambek correspondence
From HaskellWiki
m (typo) |
(Add a missing parenthesis) |
||
Line 31: | Line 31: | ||
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. |
Revision as of 11:08, 9 November 2008
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 |
1 Life, the Universe and Everything
As is well established by now,
theAnswer :: Integer theAnswer = 42
2 Inference
A (non-trivial) Haskell function maps a value (of typerepresentation :: 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 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
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 = filter (<= x) xs higher = filter (> x) xs
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.
7.1 Functional dependencies
These type level functions are set-theoretic. That is,8 Indexed types
(please someone complete this, should be quite interesting, I have no idea what it should look like logically)