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.
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
- Truth and falsehood, written as (truth) and (falsehood)
- The connectives, given two propositions lets us talk about
- and are true, written as
- or (or both) are true, written as
- Implication, given two propositions lets us talk about
- if is true then is, written as
- Negation, which given a proposition lets us talk about
- is false, written as
Combining these we can create larger propositions such as or . 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 .
Given the knowledge that a proposition is true, we may make conclusions about the propositions used to construct .
- If is true, then both and are true
- If is true, then at least one of or is true
- If is true, then must be true whenever is
- If is true, then 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 , if is true then is true since is, if is false then we need not concern ourselves with the motive of the implication. An important tautology following the same reasoning is . An example of a contradiction is , this proposition states that 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 () are interpreted as type variables
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.
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.
data Truth = TruthWitness
Translating 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.
The connectives might seem more tricky, but turn out to be fairly straightforward as well. A proof of is simply a proof of and a proof of , but wait, that’s a pair! is thus interpreted as
(P, Q). Likewise, a proof of is either a proof of or a proof of , that’s right, it’s the
Either type! is interpreted as
Either P Q.
The implication tells us that if we have a proof of then we have a proof of . So what we need is a way of turning terms of type into terms of type . 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 to be true 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 as , that is, is true if is. But since we know that is false, this means cannot be true. Thus we interpret as
P -> Falsehood. To aid readability we will make the definition below.
type Not p = p -> Falsehood
Now that we’ve introduced our language, let us speak! We shall prove the above-mentioned tautology by constructing a function
a -> Either a b. If you’ve used the
Either type before then the proof is trivial.
proof1 :: a -> Either a b proof1 = Left
Now let us prove that is a contradiction, we shall do this by proving its negation . 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.
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.
|Proof||Term (element of type)|
|$$\top$$||Type with a known term|
|$$\bot$$||Type with no terms|
|$$P \land Q$$|| |
|$$P \lor Q$$|| |
|$$P \to Q$$|| |
|$$\lnot P$$|| |
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.
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood) proof2 = undefined
And here’s another version!
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.
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
error from Haskell (in fact, these values, called 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) these programming languages necessarily place restrictions upon what programs are allowed in order to garantuee termination. Consequently, these languages are not Turing-complete, 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 and . Proving these classically is trivial, just consider the case where is true, and the case where is false, in both cases these propositions hold. In Haskell however, it’s trickier, think about it, how could one write these programs?
impossible1 :: Not (Not a) -> a -- ((a -> Falsehood) -> Falsehood) -> a impossible2 :: Either a (Not a) -- Either a (a -> Falsehood)
These two propositions have names, is called the law of excluded middle, and 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.
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. 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, 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.
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 to those familiar with Haskell; a lengthy list of agda tutorials 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, HoTTEST Summer School 2022 GitHub, Introduction to Homotopy Type Theory, 1lab, HoTT Book.