155 lines
14 KiB
Markdown
155 lines
14 KiB
Markdown
---
|
|
layout: post
|
|
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 the Curry-Howard isomorphism.
|
|
|
|
<!--more-->
|
|
|
|
{% katexmm %}
|
|
|
|
## What is logic?
|
|
|
|
Before we can talk about logic in Haskell we have to talk about propositional logic. Propositional logic is a set of rules telling us how to construct propositions, and how to derive conclusions from true ones.
|
|
|
|
First, we shall get a feel for what a proposition is by breaking down some examples. Consider the following statements: "It is sunny outside", "The bank is open", "It is either sunny or rainy outside", and "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. Let us then specify the forms a propositions may have.
|
|
|
|
* The atomic propositions, which we shall call $a, b, c \dots$
|
|
* Truth and falsehood, written as $\top$ (truth) and $\bot$ (falsehood)
|
|
* The connectives, given 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, given 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})$.
|
|
|
|
Given the knowledge that a proposition $P$ is true, we may make conclusions about the propositions used to construct $P$.
|
|
|
|
* If $P \land Q$ is true, then both $P$ and $Q$ are true
|
|
* If $P \lor Q$ is true, then at least one of $P$ or $Q$ is true
|
|
* If $P \to Q$ is true, then $Q$ must be true whenever $P$ is
|
|
* If $\lnot P$ is true, then $P$ is false
|
|
|
|
To prove things one more concept needs to be introduced, that of tautologies and contradictions. A tautology is a statement that is true no matter if the atoms inside of it are true or not, and conversely, a contradiction is a statement that 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 ourselves with the motive of the implication. An important tautology following the same reasoning is $\bot \to P$. An example of a contradiction is $a \land \lnot a$, this proposition states that $a$ is both true and false, which is impossible.
|
|
|
|
In logic we are usually interested in proving that a proposition is either a tautology or a contradiction, proving or disproving its truth. One usually does this by following the rules of the logic, repeatedly applying them to yield a proof. However there is another way to do logic, through Haskell!
|
|
|
|
## Interpreting logic in Haskell
|
|
|
|
How does one translate from propositional logic to Haskell? We shall interpret types as propositions, and terms (elements) of a type as witnesses or proofs that the proposition (the type they inhabit) is true. The typechecking of Haskell will then double as a proof checker. This might seem abstract at first, but once you see how the building blocks of propositions translate into types it will become clear.
|
|
|
|
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`, since one would have to create a proof `p :: a`, that is, a term inhabiting every type. This corresponds to how one cannot prove or disprove atomic propositions in propositional logic.
|
|
|
|
$\top$ may be interpreted as any type of which we know a term, that is, any proposition of which we know a proof. For the sake of readability we shall define a 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 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 straightforward 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 thus 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$. That is, a function `P -> Q`, would you look at that, it's even the same arrow!
|
|
|
|
Perhaps surprisingly the trickiest part of the translation is negation. For $\lnot P$ to be true $P$ must be false, that is, there may not be any 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`. To aid readability we will make the definition below.
|
|
```hs
|
|
type Not p = p -> Falsehood
|
|
```
|
|
|
|
Now that we've introduced our language, let us speak! We shall prove the above-mentioned tautology $a \to 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 its negation $\lnot (a \land \lnot a)$. In doing so we need to construct a term of type `Not (a, Not a)`, that is, `(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, coming up with some propositions and proving them by hand and using Haskell. The table below gives an overview of the translation from logic to Haskell.
|
|
|
|
<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 a 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
|
|
|
|
I admit, we did use a little too much effort when constructing `proof2`, there is a more succinct version, which type checks all the same.
|
|
```hs
|
|
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 both of these typecheck, we understand that they are not valid proofs, in fact, we can prove `Falsehood` in this exact way.
|
|
```hs
|
|
proof3 :: Falsehood
|
|
proof3 = proof3
|
|
```
|
|
This is not good, maybe programming languages don't correspond to logic after all? The solution is to "run" our proofs 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.
|
|
|
|
The programming languages studied by logicians guarantee termination and don't include values like `undefined` or `error` from Haskell (in fact, these values, called [bottom](https://wiki.haskell.org/Bottom), exist to model non-terminating programs). These programming languages, while they can check proofs entirely during typechecking, come with their 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 in order to garantuee termination. Consequently, these languages are not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness), meaning there are programs one cannot write in the language.
|
|
|
|
## Excluding the middle
|
|
|
|
The logic which we do in Haskell has a name, it's called constructive logic. The name is due to the fact that one must "construct" a proof, such as a function, in order to prove a theorem. Every theorem has an explicit construction that shows us how the proof is performed. This requirement, as it turns out, is quite strict, so strict that we can no longer prove all the things we could in classical logic. In particular, we will be unable to prove both $\lnot \lnot P \to P$ and $P \lor \lnot P$. Proving these classically is trivial, just consider the case where $P$ is true, and the case where $P$ is false, in both cases these propositions hold. In Haskell however, it's trickier, think about it, how could one write these programs?
|
|
```hs
|
|
impossible1 :: Not (Not a) -> a -- ((a -> Falsehood) -> Falsehood) -> a
|
|
impossible2 :: Either a (Not a) -- Either a (a -> Falsehood)
|
|
```
|
|
|
|
These two propositions have names, $P \lor \lnot P$ is called the law of excluded middle, and $\lnot \lnot P \to P$ is called double negation. Though it might not be obvious, double negation follows from excluded middle. By assuming excluded middle, we can even use Haskell to prove this.
|
|
|
|
```hs
|
|
assume_excluded_middle :: Either a (Not a)
|
|
assume_excluded_middle = error "Proof depends on excluded middle"
|
|
|
|
-- Since there are no values of Falsehood this is a perfectly
|
|
-- fine constructive definition. One cannot call this function
|
|
-- without already using an error or infinite loop.
|
|
-- Proof-oriented programming languages will let you construct
|
|
-- a function of this type without using `error`.
|
|
if_pigs_fly :: Falsehood -> a
|
|
if_pigs_fly f = error "cannot happen"
|
|
|
|
double_negation :: Not (Not a) -> a
|
|
double_negation notnota = case assume_excluded_middle of
|
|
Left a -> a
|
|
Right nota -> if_pigs_fly (notnota nota)
|
|
```
|
|
|
|
In Haskell our propositions are types, which carry proofs around. We cannot simply assume that any proposition must be true or false, because in doing so one would have to either produce a proof that it is true, or a proof that it is false. This is the very reason we are not able to prove excluded middle, as well as the reason that double negation follows from excluded middle. Excluded middle is the very rule telling us that we may assume every proposition is either true or false, excluding the possibility of a middle value.
|
|
|
|
Logicians have given a name to logics in which one cannot prove excluded middle, these logics are called intuitionistic. Initially it might be confusing why one would wish to work in a logic where not every proposition may be assumed to be either true or false, such a fact seems obvious. Likewise, mathematicians have historically been [at each other arguing over the validity of excluded middle](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy#Validity_of_the_law_of_excluded_middle). Though intuitionistic logic might seem counter-productive there are today multitudes of reasons to work without excluded middle. A philosophical reason is provided by [Gödel's incompleteness theorem](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Completeness), which states that in all sufficiently powerful systems of logic there will be statements that are neither provable nor disprovable. In the presence of this knowledge, it might be unsettling that excluded middle lets one assume these statements are either true or false. There are also practical reasons to work in intuitionistic logic. There are a lot of objects in mathematics that interpret intuitionistic logic (such as Haskell), meaning results in intuitionistic logic apply to more of mathematics. Generality is the true strength of intuitionism. An intuitionistic proof holds in a classical setting, but a classical proof may not be interpreted intuitionistically.
|
|
|
|
## Wrapping up
|
|
|
|
If you've made it this far, then congratulations! Even though I've tried to make this blog post introductory it's by no means trivial. Hopefully you are now feeling the same wonder as I did when stumbling into this topic. I'd like to end by broadly writing about where one might head next.
|
|
|
|
This blog post only covers propositional logic, but one can interpret predicate logic and even higher-order logic within programming languages. This is done with dependent type theory. In dependent type theories, types may themselves *depend* upon values, letting one create types such as `is-even n` which depend on a natural number `n`. This type would have terms which are witnesses that `n` is even. These programming languages, or proof assistants as they are usually called, enable you to prove properties of both programs and mathematical objects. In doing so they provide a way to automatically check mathematical proofs for correctness. There are already many mathematicians using these tools to create formalized proofs of mathematical theorems.
|
|
|
|
If you are interested in learning more about dependent type theory, then you might be interested in downloading and playing around with a proof assistant. I recommend [agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) to those familiar with Haskell; a lengthy [list of agda tutorials](https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html) is included in its documentation. If you wish to learn more about how doing math with types rather than sets might lead to new insights and connections to topology, then I encourage you to learn about homotopy type theory, for which there are some great resources: [HoTTEST Summer School 2022 lectures](https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx), [HoTTEST Summer School 2022 GitHub](https://github.com/martinescardo/HoTTEST-Summer-School), [Introduction to Homotopy Type Theory](https://arxiv.org/abs/2212.11082), [1lab](https://1lab.dev/1Lab.intro.html), [HoTT Book](https://homotopytypetheory.org/book/).
|
|
|
|
{% endkatexmm %}
|