Initial commit.

Curry-Howard-Lambek Correspondence.page

@@ -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)*
+
+

FrontPage

@@ -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/
+