rachel.cafe/_posts/2022-12-15-haskell-and-logic.md

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.

{% 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.

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.

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.

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.

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.

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.

Logic	Haskell
Proposition	Type
Proof	Term (element of type)
Atom	Type variable
\top	Type with a known term
\bot	Type with no terms
P \land Q	(P, Q)
P \lor Q	Either P Q
P \to Q	P -> Q
\lnot P	P -> EmptyType

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 undefined or 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 \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?

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.

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.

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 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.

{% endkatexmm %}