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.