jgm/gitit

Initial commit.

• Loading branch information...
jgm committed Nov 7, 2008
0 parents commit 89725fd92c3cb99f7825dcc93c25a8f40918b2f2
 @@ -0,0 +1,191 @@ +# 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 +declaration: + +~~~ {.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)* + +
 @@ -0,0 +1,32 @@ +# Welcome to Gitit! + +Gitit is a [Wiki] written in [Haskell]. [HAppS] is used for the web +server and session state. Pages and uploaded files are stored in a [git] +repository and may be modified either by using git's command-line tools +or through the wiki's web interface. [Pandoc]'s extended version of +[markdown] is used as a markup language. Gitit can be configured to +display TeX math and highlighted source code. + +You can edit this page by double-clicking on it, or by clicking on the +"edit" button at the bottom of the screen. + +You can make a link to another wiki page like this: +[French Cheeses](). +This will produce a link like this: [French Cheeses](). Note that +the names of wiki pages need not be in CamelCase, and they may contain +spaces. Wiki pages may be organized into directories. Use the +slash ("/") character between directories and page names or +subdirectories: [Wines/Pinot Noir](). + +To create a new wiki page, just create a link to it and follow +the link. + +Help is always available through the "help" link on the top bar. + +[Wiki]: http://en.wikipedia.org/wiki/Wiki +[git]: http://git.or.cz/ +[HAppS]: http://happs.org +[Haskell]: http://www.haskell.org/ +[pandoc]: http://johnmacfarlane.net/pandoc/ +[markdown]: http://daringfireball.net/projects/markdown/ +

0 comments on commit 89725fd

Please sign in to comment.