Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
192 lines (152 sloc) 6.99 KB
# Curry-Howard-Lambek Correspondence
The Curry-Howard-Lambek correspondence 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).
## Life, the Universe and Everything
As is well established by now,
~~~ {.literatehaskell}
> 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).
A (non-trivial) 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).
~~~ {.haskell}
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 $\wedge$ and
$\vee$, though heavily disguised. Haskell handles $\vee$ conjuction in the
manner described by Intuitionistic Logic. When a program has type $A \vee B$,
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:
~~~ {.literatehaskell}
> 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."
~~~ {.haskell}
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...
~~~ {.literatehaskell}
> show :: Message String -> String
> show (OK s) = s
> show (Warning s) = "Warning: " ++ s
> show (Error s) = "ERROR! " ++ s
The $\wedge$ conjuction is handled via an isomorphism in Closed Cartesian
Categories in general (Haskell types belong to this category):
$\mathrm{Hom}(X\times Y,Z) \cong \mathrm{Hom}(X,Z^Y)$. That is, instead of
a function from $X \times Y$ to $Z$, we can have a function that takes an
argument of type $X$ and returns another function of type $Y \rightarrow Z$,
that is, a function that takes $Y$ to give (finally) a result of type
$Z$: this technique is (known as currying) logically means
$A \wedge B \rightarrow C \equiv A \rightarrow (B \rightarrow C)$.
(insert quasi-funny example here)
So in Haskell, currying takes care of the $\wedge$ connective. Logically,
a proof of $A \wedge B$ 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.
# Theorems for free!
Things get interesting when polymorphism comes in. The composition
operator in Haskell proves a very simple theorem.
~~~ {.literatehaskell}
> (.) :: (a -> b) -> (b -> c) -> (a -> c)
>(.) f g x = f (g x)
The type is, actually, `forall a b c. (a -> b) -> (b -> c) -> (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.
~~~ {.literatehaskell}
> 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.
~~~ {.literatehaskell}
> 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
~~~ {.literatehaskell}
> instance Eq Bool where
> True == True = True
> False == False = True
> _ == _ = False
> (/=) a b = not (a == b)
A not-so-efficient sort implementation would be:
~~~ {.literatehaskell}
> sort [] = []
> sort (x : xs) = sort lower ++ [x] ++ sort higher
> where lower = filter (<= x) xs
> higher = filter (> 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.
# 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, 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)*
Jump to Line
Something went wrong with that request. Please try again.