write a lot on haskell and logic draft

_drafts/haskell-and-logic.md

@@ -1,9 +1,9 @@
 ---
 layout: post
-title: "Haskell and Logic?"
+title: "Haskell and Logic"
 ---
 
-Haskell programs are proofs, don't you know? Hidden inside the types of Haskell lies a deep connection to mathematical logic. Given some basic Haskell knowledge and mathematical interest you too may experience the sense of wonder I first did when discovering this topic.
+Haskell programs are proofs, don't you know? Hidden inside the types of Haskell lies a deep connection to mathematical logic. Given some basic Haskell knowledge and mathematical interest you too may experience the sense of wonder I first did when discovering the Curry-Howard isomorphism.
 
 <!--more-->
 
@@ -11,38 +11,117 @@ Haskell programs are proofs, don't you know? Hidden inside the types of Haskell
 
 ## What is logic?
 
-* Propositional logic
+Before we can talk about logic in Haskell we have to talk about logic itself. While most of us have an intuition for what is logical it might be hard to formalise. This blog post will mainly concern itself with propositional logic. Propositional logic is made up by a set of rules telling us how to construct propositions, and how to derive conclusions from true propositions.
-* Truth, Falsehood
-* Connectives, Negation and Implication
-* Truth Tables?
 
-* What does this have to do with Haskell?
+The following are some examples of propositions: "It is sunny outside", "The bank is open", "It is either sunny or rainy outside", "If it is rainy then the bank is not open". The first two statements are "atomic", they cannot be broken down into smaller propositions, unlike the latter two statements which are built up from smaller propositions. In addition to atoms there are the connectives 'and', 'or'; negation and implication. Additionally there is a true and a false proposition. Let us then specify which propositions we may form.
+
+* The atomic propositions, which we will call $a, b, c \dots$
+* Truth and falsehood, written as $\top$ (truth) and $\bot$ (falsehood)
+* The connectives, which given any two propositions $P, Q$ lets us talk about
+  * $P$ and $Q$ are true, written as $P \land Q$
+  * $P$ or $Q$ (or both) are true, written as $P \lor Q$
+* Implication, which given any two propositions $P, Q$ lets us talk about
+  * if $P$ is true then $Q$ is, written as $P \to Q$
+* Negation, which given a proposition $P$ lets us talk about
+  * $P$ is false, written as $\lnot P$
+
+Combining these we can create larger propositions such as $a \to a \lor b$ or $a \lor (b \land \lnot c)$. We can now translate English non-atomic propositions into the language of propositional logic. "If it is rainy then the bank is not open" becomes $\textrm{it is rainy} \to \lnot (\textrm{bank is open})$.
+
+Now given the knowledge that a proposition $P$ is true, we can draw conclusions about the propositions used to construct $P$. 
+
+* If $P \land Q$ is true, then we know that both $P$ and $Q$ are true
+* If $P \lor Q$ is true, then we know that at least one of $P$ or $Q$ is true
+* If $P \to Q$ is true, and $P$ is true, then $Q$ is true
+* If $\lnot P$ is true, then $P$ is false
+
+There is one more concept I must introduce in order to make proving things interesting, which is that of tautologies and contradictions. A tautology is a statement which is true no matter if the atoms inside of it are true or not, and conversely a contradiction is a statement which is always false. An example of a tautology is $a \to a \lor b$: if $a$ is true then $a \lor b$ is true since $a$ is, if $a$ is false then we need not concern ourself with the motive of the implication. An example of a contradiction is $a \land \lnot a$, this proposition states that $a$ is both true and false, which is impossible. 
+
+When we are doing logic we are usually interested in proving that a proposition is either a tautology or a contradiction given a list of propositions declared to be true. One usually does this by following the rules of logic, which I have sketched out above, reaching conclusions based on hypotheses the hypotheses until one arrives at a conclusion. However, as I am about to show you, there is another way to do logic, through Haskell!
 
 ## Interpreting logic in Haskell
 
-* Types as propositions
+How does one begin to translate from propositional logic to Haskell? We will interpret propositions as types, and terms (elements) of a type as witnesses/proofs that the proposition is true. The computer typechecking our program will then serve as checking that our proof is correct, allowing us to automatically check if proofs are correct. While this might seem abstract at first it will become clear once you see how we translate propositions into Haskell.
-  * Programs as Proofs
+
-* Interpretation of sentences
+Atomic propositions ($a,b,c,\dots$) are interpreted as type variables `a`, `b`, `c`, etc. You might notice that there is no way to prove `a`. This is because to prove `a` in Haskell we have to create some proof `p :: a`, but since `a` could be any type we have no way of doing this. This corresponds to how cannot prove or disprove atomic propositions without drawing conclusion from other propositions in classical logic.
+
+$\top$ may be interpreted as any type which we know a term of. For the sake of readability we define our own truth type, with a single constructor bearing witness to its truth:
+```hs
+data Truth = TruthWitness
+```
+Translating $\bot$ might seem more tricky, but it turns out Haskell actually lets us define empty types without constructors, that is, a proposition with no proof. We thus define the following:
+```hs
+data Falsehood
+```
+
+The connectives might seem more tricky, but turn out to be fairly straight forward as well. A proof of $P \land Q$ is simply a proof of $P$ and a proof of $Q$, but wait, that's a pair! $P \land Q$ is then interpreted as `(P, Q)`. Likewise a proof of $P \lor Q$ is *either* a proof of $P$ or a proof of $Q$, that's right, it's the `Either` type! $P \lor Q$ is interpreted as `Either P Q`.
+
+The implication $P \to Q$ tells us that if we have a proof of $P$ then we have a proof of $Q$. So what we need is a way of turning terms of type $P$ into terms of type $Q$. We need a function `P -> Q`, and would you look at that, it's even the same arrow!
+
+Perhaps surprisingly negation is the trickiest part of the translation. For $\lnot P$ to be true $P$ must be false, that is, there are no terms `p :: P` bearing witness to the truth of P. How can we express this within Haskell? The trick is to redefine $\lnot P$ as $P \to \bot$, that is, $\bot$ is true if $P$ is. But since we *know* that $\bot$ is false, this means $P$ cannot be true. Thus we interpret $\lnot P$ as `P -> Falsehood`. In order to aid readability we will make the following definition:
+```
+type Not p = p -> Falsehood
+```
+
+Now that we've introduced our language, let us speak! We shall prove the above mentioned tautology $a -> a \lor b$, by constructing a function `a -> Either a b`. If you've used the `Either` type before then the proof is trivial.
+```hs
+proof1 :: a -> Either a b
+proof1 = Left
+```
+
+Now let us prove that $a \land \lnot a$ is a contradiction, we shall do this by proving $\lnot (a \land \lnot a)$. In doing so we need to construct a term of type `Not (a, Not a)`, which after we unwrap the definition of `Not` becomes `(a, a -> Falsehood) -> Falsehood`. Thus, we must construct a function to `Falsehood`, which has no inhabitants, however, we are given a function `a -> Falsehood` which we may use to get a term of the empty `Falsehood` type, by applying the supplied value of type `a` to it.
+```hs
+proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
+proof2 (a, f) = f a
+```
+
+I strongly encourage you to play around with this on your own, trying to come up with some propositions and proving them by hand and with Haskell. The table below is gives an overview of the translation.
+
+<table>
+<tr> <th>Logic</th> <th>Haskell</th> </tr>
+<tr> <td>Proposition</td> <td>Type</td> </tr>
+<tr> <td>Proof</td> <td>Term (element of type)</td> </tr>
+<tr> <td>Atom</td> <td>Type variable</td> </tr>
+<tr> <td>$\top$</td> <td>Type with known term</td> </tr>
+<tr> <td>$\bot$</td> <td>Type with no terms</td> </tr>
+<tr> <td>$P \land Q$</td> <td><code>(P, Q)</code></td> </tr>
+<tr> <td>$P \lor Q$</td> <td><code>Either P Q</code></td> </tr>
+<tr> <td>$P \to Q$</td> <td><code>P -> Q</code></td> </tr>
+<tr> <td>$\lnot P$</td> <td><code>P -> EmptyType</code></td> </tr>
+</table>
+
 
 ## The paradoxes of Haskell
 
-* Bottom/Undefined
+I admit, we did use a little too much effort in the previous section when constructing `proof2`, here is a more succinct version, which type checks all the same:
-* Recursion
+```hs
-* Checking proofs in Haskell (having to evaluate them)
+proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
+proof2 = undefined
+```
+And here's another version
+```hs
+proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
+proof2 = proof2
+```
+While all of these typecheck we understand that they are not valid proofs, in fact we could prove `Falsehood` in this exact way.
+```
+proof3 :: Falsehood
+proof3 = proof3
+```
+Well, this is no good, maybe programming languages don't correspond to logic after all? Luckily there is both a solution to this problem. The solution is to "run" our proofs in order to check them, proofs defined this way will either crash or loop forever, so once we see that our proof terminates then we know the proof to be correct. 
+
+Programming languages studied by logicians usually guarantee termination and don't include values like `undefined` or `error` from Haskell (in fact, the very reason these exist in Haskell is to model non-terminating programs). These programming languages, while they are able to check proofs entirely during typechecking come with their own limitations. Since there is no way to decide if an arbitrary program will terminate ([the halting problem](https://en.wikipedia.org/wiki/Halting_problem)) these programming languages necessarily place restrictions upon what programs are allowed. Consequently these languages are not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness), meaning there are programs one cannot write in the language.
 
 ## Intuitionism
 
 * Cannot prove all things from logic
-* Our truthtables are an oversimplification
+* Boolean logic is an oversimplification
 * Broader logic needed, intutionistic logic
-  * Liknelse till kommutativitet från gruppteori?
 
 ## The Horizon: Type theory
 
 * Quick recap, where does one go from here though? (överkurs)
 * But how does one interpret higher order logic?
 * Pi and Sigma types
-* Equality types
+* Equality types?
-* Quick comment on HoTT
 
 {% endkatexmm %}

assets/css/main.scss

@@ -125,16 +125,17 @@ nav ul li {
 	white-space: nowrap;
 }
 
-nav ul li a {
-	color: gray;
-}
-
 hr {
 	color: gray;
 	border: 0;
 	border-bottom: 1px dashed; 
 }
 
+table {
+  margin-left: auto;
+  margin-right: auto;
+}
+
 .centercol {
 	width: 50em;
 	max-width: 94vw;