Language Features

There's a Mathematician In Your Compiler

Illustrated by Skye Bolluyt

People with an interest or education in computer science may know about the Curry-Howard isomorphism, the correspondence between (pure) types in typed languages and logic: statements, propositions, proofs. A pure function is one with no side effects, no exceptions, and for the purposes of this article, no infinite recursion. A pure value would just be a value.

But what use is that to me, your average hard-working, yet underpaid, developer? I hear you ask. Is there a practical use of this in everyday programming?

It may not be of use in everyday programming when you are figuring out how to implement a Google API. But recognizing it and how it relates to patterns the compiler forces you into will certainly make you a better programmer, and we can discover cool new language features using it.


You may find the full source code of this article on GitHub: https://github.com/HumanReadableIO/hrm-code/tree/master/theres-a-mathematician-in-your-compiler

We'll be taking a whistlestop tour of the Curry-Howard isomorphism and how it relates to Scala. By the end of this article we will have deduced surprising new Scala functionality (type negation) using only basic knowledge of Scala and logic.

In this article I will endeavor to refer to logical true and false as True and False to distinguish them from the Scala values true and false.

If you need a quick refresher on logical True and False, here it is: The logical proposition True simply represents something that is true, like the statement 1 < 5. Any true statement like that by definition implies True. If we can start from an assumption and perform a series of logical deductions and reach True, then we know our original assumption is True, that it is provable. Conversely, any statement we know or can prove to be wrong (such as "bananas are a myth") implies False. If we can reach False at the end of a series of logical deductions from an assumption, our assumption is incorrect.

They're the Type That Gets Propositioned

The basic concept of the Curry-Howard isomorphism is really very simple. A logical proposition A can be equated to some type, say trait A. Logical propositions are made up of propositions P, Q, and more, and the operations => (implies), & (and), | (or), and ! (negation). There are more formal (unicode) symbols we could use, but these are universal enough and get the point across just as well.

The logical proposition A is considered True if and only if it can be proved, a true theorem following the rules of mathematical logic (reaching your conclusion A through a series of valid logical deductions and substitutions, starting from assumed truths).

Equivalently, proposition A evaluates to True (or is provable) if and only if the equivalent Scala type trait A representing proposition A has at least one value. We say the type trait A is inhabited if it has at least one value.

The same idea extends to logical implication statements: the logical implication A => B holds true if and only if there exists a pure function of type Function1[A, B], where A and B here are the Scala types equivalent to our original logical propositions. In Scala, this function type can of course be rewritten as A => B. It's no coincidence the authors of Scala chose the symbol for logical implication as their symbol for function definition.

Truth

Here we'll go through a quick example to see how to turn logical statements into pure Scala code via the Curry-Howard isomorphism. We'll be considering logical True.

In real life, any 'true' statement is considered True-"Apples exist," for example. What does True translate to in Scala under the Curry-Howard isomorphism?

It needs to be a type that is inhabited, that has a value. By convention we choose Unit, the type with one member whose value is denoted (). This is the same as Java's void. We could choose any inhabited type we like, including Int or Boolean. But it's tidier to choose Unit because you can always write the function A => Unit uniquely, for any A, by simply ignoring the argument and returning (). This makes it more canonical; there are fewer choices to make.

To summarize: by convention we'll say that True maps to Unit.

And Falsehood

And another, slightly more subtle example of how to reason about this correspondence: How do we translate False into pure Scala code?

We need to map it to some type in Scala, but remember that a proposition is provable if the corresponding type has any values associated with it.

And False certainly is not provable. A false statement may be "bananas are a myth."

Luckily there is one uninhabited type in Scala: Nothing. It is the type of a thrown Exception, the bottom of the type tree. (Or the top, if you're the sort who views the type tree upside down.)

You can never implement a pure function A => Nothing, for an inhabited type A, as there are no values to return. A function of this signature, when called, would either terminate the program (i.e., throw an exception) or never finish computing. In the same way, you can never prove a statement A => false for any non-False A. A real-life example of such absurdity would be "Apples exist, therefore the dairy industry is poisoning our children."

Interestingly, the logical statement False => False is provable. (If a false statement is assumed true, such as "Bananas are mythical," then you can prove any statement you like, including false ones.) This means there must be a well-defined and inhabited pure Scala type associated with it. What could this be?

It is simply the identity function of type Nothing => Nothing. This is, a little surprisingly, well-defined and pure. Even though it returns something that cannot exist, it also accepts an argument that cannot exist and therefore can never be called. It certainly exists, but it can never cause you any problems.

Writing a Proof

Well, the upshot of all of this is that every time you write a pure function of type A => B in Scala, you are actually writing a proof:
A implies B. This makes sense: in a function you are assuming you have been given a value of type A (i.e., assuming type A is inhabited, and thus assuming proposition A is provable) and you are producing a value of type B, which would make B inhabited-and thus also provable.

For example, a simple tuple manipulation:

def swap[A, B](tuple: (A, B)): (B, A) = (tuple._2, tuple._1)

It's important to note above that A and B are type parameters; they are not fixed. Curry-Howard is a very general theorem. This function is equated to the proposition

A & B => B & A

which is obviously true to us, as normal, functioning humans (if I have an apple and a banana, then I have a banana and an apple). But because it's not obvious to mathematicians, you can also write a formal logical proof of this statement. But that's tangential to this article, so I won't go into it. The proof could eventually be equated to the implementation of swap anyway.

How about a statement that is not provable?

A => A & B

We simply don't know if this is provable for a general B. If I have an apple, it does not imply I have an apple and a banana. I do actually happen to have an apple and a banana, but you can't prove it from just the apple.

It would map to the Scala function:

def beify[A, B](a: A): (A, B) = ...

When is this implementable? You don't have a B! You cannot implement it for a general type B, only when B evaluates to True:

// Perfectly well-defined
def beify[A](a: A): (A, Unit) = (a, ())

And this of course corresponds to

A => A & True

So things are looking pretty consistent so far. Let's do something a little more fun.

Prove It

The Scala compiler is, in rather loose terms, a theorem prover. We saw above that the compiler will check and verify your proofs for you, if you write the functions out yourself. But the compiler can also write the proofs for you.

The implicit keyword is the key to this functionality.

When you ask the compiler for an implicit value of type A, it will search all available implicit values and functions, and try to fit them together to create a value of type A, to prove the proposition A, automatically.

A brief example:

implicit val i: Int = 7
implicitly[Int]  // Returns 7

Pretty trivial: if you provide a value of type Int to the compiler, it can 'prove' Int is true by simply returning that value.

A slightly more complex example:

implicit def foo(implicit i: Int): String = i.toString

implicit val i: Int = 19

implicitly[String]  // Returns "19"

What have we done here? We've defined a proposition Int by providing a value 19 and defined an implication Int => String with the functionality _.toString. And, therefore, the compiler can prove proposition String by providing the value "19".

This is pretty powerful. It looks a little vapid because we hard-coded Int at 19. But it needn't be hard-coded, and could instead rely on very complex machinery under the hood.

Let's try to do something cool.

We Don't Want Your Type in Here

Let's try to make a function that accepts any type except B (for some given B) in a general way. We want to be able to write:

def foo[A](a: A)(implicit proof: IsNot[A, B]): String = a.toString + " is not a B!"

Every time we call foo, we want the compiler to provide us a proof that A is not B. We're wrapping this up inside a type class we're calling IsNot. If the compiler cannot define IsNot[A, B], that is, cannot prove A is not B, we expect compilation to fail. We only want this to happen when they are indeed equal.

We don't have many choices about how IsNot will look. It must be something like the following:

trait IsNot[A, B]

Now we just need to give the compiler some predicates (implicits) about how to find proofs that show types aren't equal to each other.

It turns out this is "difficult" in a computer language. We can't just implement an implicit instance of IsNot for every unequal pair of types in existence. There are many types after all; it would take too long. Some even say there are an infinite number of them.

Thankfully, because the Scala compiler is a pure and deterministic (though not necessarily predictable) process, it will always produce the same output. It will make only well-defined and repeatable choices. If it can't make such a choice, it will exit.

One such scenario in which compilation will fail is if there are two implicits for the same type at the same level, and you request the compiler find a proof of the type:

trait A

implicit val intProof: Int = 17

implicit def instance1(implicit b: Int): A = new A {}
implicit def instance2(implicit b: Int): A = new A {}

implicitly[A]  // fails, warning about 'ambiguous' implicits

How can the compiler choose between instance1 and instance2? It can't; there's literally nothing to choose between. They are the same. It fails compilation, saying there are ambiguous implicits.

In this scenario, when there is more than one proposition implying A and you ask it to prove A, the compiler takes them all and combines their left-hand sides using XOR to get one single proposition implying A. (XOR being an operation that resolves to True if and only if precisely one of its two operands is True.)

(In reality there are a hierarchy of implicit search locations the compiler tries in order, with ranks for specificity and all sorts of exotic things, forming more complex compiled propositions with more verbs than just XOR. But in this scenario, the left-hand sides are indeed joined inside an XOR.)

In the above example, the compiler compiles the following:

(Int XOR Int) => A

And this of course reduces to just False => A, which is simply True-which is emphatically not a proof of A (it is a tautological proof of True). And thus, the compiler declares A unprovable. It tried its best, but the compiler was unable to find a canonical proof of A.

How does this apply to IsNot? We're going to reason about some logic, and then from that implement IsNot and see it working.

We're trying to prove proposition A IsNot B when A is not equal to B. That is:

(A != B) => A IsNot B

We have to manipulate this in some way to make it something we can backport to Scala. We can't use A != B directly, since that's what we're trying to implement.

Well, there's a handy identity that P <=> true xor !P for any proposition P. Making that substitution on the left we get

(True xor A=B) => A IsNot B

This is suddenly in a form we can work with-we can turn these two terms into Scala implicits. We'll end up with two implicits, both of which return A IsNot B. One will take an implicit proof that A = B (provided to us by Scala), and one that takes a vacuous implicit True-in other words, no argument list needed (or the always available and fantastically named DummyImplicit type that native Scala supplies us).

And here they are; the code by this point writes itself:

implicit def instanceAll[A, B]: A IsNot B = new IsNot[A, B] {}

// Equivalently the above could be `implicit def instanceAll[A, B](implicit True: DummyImplicit): A IsNot B = new IsNot[A, B] {}`

implicit def instanceEquality[A, B](implicit proof: A =:= B): A IsNot B = new IsNot[A, B] {}

And here it is working, proof (pun intended) that I haven't been lying to you:

// The forbidden type:
trait B

def foo[A](a: A)(implicit proof: IsNot[A, B]): String = a.toString + " is not a B!"

foo(5)           // compiles
foo("a string")  // compiles
foo(new B {})    // Does not compile: Compiler cannot prove B is not B!

And as a little bonus, you can even chain the required proofs and have more than one requirement:

def bar[A](a: A)(implicit
  proof1: A IsNot Int,
  proof2: A IsNot String
): String = a.toString

bar(true)  // compiles
bar(4)     // no bueno
bar("4")   // no bueno

Author's Note

We can obviously just create a value of type IsNot[A, B] for any A and B we like, whenever we like, if we wanted to thoroughly ruin things. It only works because the implicit modifiers are markers to the future coder: let the compiler provide these proofs for us.

End Author's Note

We've managed to prove a negative here, working at a purely logical level and a very basic understanding of how Scala interprets logical statements. Hardly any actual Scala knowledge needed at all!

If you look closely at the implicits we did end up defining, they don't make much sense on their own. The first one after all is rather nonsensically saying A IsNot B, for all A and B. And the second one causes a compiler crash (with a very bad compile error message) in order to short-circuit the compiler and cause an end to compilation in certain circumstances.

The runtime interpretation of the code we've written feels very hacky, but the maths behind it that we demonstrated above are solid, and hopefully show we've discovered functionality of the language itself. That's pretty cool.

James Phillips

author

James is a functional and scala enthusiast with a keen interest in type-level programming. He runs a consultancy in London and Brighton, and occasionally cycles to Paris.

Skye Bolluyt

illustrator

Skye Bolluyt is a NYC based illustrator who thrives on giving invisible moods visual expressions, through a bold yet detailed style that packs a punch without loss of nuance. Skye is insatiably curious, so her work has been published in a variety of magazines, advertising campaigns, and children’s books - the likes of Communication Arts, Juxtapoz, Portland Mercury, Pinna podcasts, 3x3 Magazine, Growing IQ LLC, among others.