Boolean Logic Using the Scala Compiler

Jack Wheatley
May 28, 2019 · 7 min read
“Contrariwise,” continued Tweedledee, “if it was so, it might be; and if it were so, it would be; but as it isn’t, it ain’t. That’s logic.” — Lewis Carroll, Through the Looking Glass

As a long-time fan of logic, and a more recent fan of type-level programming, I thought it only proper that I combine the two, and that’s exactly what we’re going to do!

The aim of this project is to codify boolean logic at the type-level in Scala, thus allowing us to evaluate the truth of expressions, and show whether boolean functions are satisfiable or tautological, all at compile-time. And if any of this logical terminology is unfamiliar to you, I hope you will have a better idea by the end.

Getting the language

Next, we want to be able to perform operations on booleans, much like we would in runtime code. So we define the following operations:

From this we can build up complex expressions like:

~[True & False] | (False -> (True & ~False))

Truth of Expressions

The idea being that our function is going to look like:

def isTrue[E <: Expression](implicit t: Truth[E]) = ???

So, first to the implicits for Truth[E]:

The Truth implicits are easy enough to reason through:

  • True must always be true, so it has an implicit defined
  • False must never be true, so it doesn’t have an implicit
  • ![E] is true only in the case where E is false
  • E1 & E2 is true only in the case where both E1 and E2 are true

We can also see that is isn’t just enough to define the conditions under which expressions are true, as ![E] requires evaluating the falseness of E . So onto the Falseness implicits:

The cases for False, True and ! are straightforward, as before. & is more interesting though, as there are 3 different conditions under which an & expression can be false:

  1. left expression is false, right is true
  2. right expression is false, left is true
  3. both expressions are false

This can be reduced to the two implicit definitions we see above: andLeftFalseness checks whether the left-hand expression is false, which covers cases 1 and 3. andRightFalseness covers the remaining case 2 where the left is true, but the right is false. If we have set everything up correctly these implicits will never clash, as it shouldn’t be possible for an expression to have implicit Truth and Falseness defined for an expression simultaneously. (If this were possible, either we have done something terribly wrong, or logic itself is inconsistent, and my money would be on us having messed up.)

With these in place we can try out our function:

Boolean Functions

def foo(a: Boolean, b: Boolean, c:Boolean): Boolean

There are two terms that we are going to use a lot going forward: tautology and satisfiable. A boolean function is a tautology if it is always true; no matter the values you put in for a, b, c, etc., the function always returns true. A boolean function is satisfiable if for some input values it returns true. Our goal in the following section will be to try and lift these concepts to the type-level, leveraging what we achieved in the previous section.

To represent functions at the type-level, we will use higher-kinded types; things that look like E[_,_]. You may notice that we’ve already got a few higher-kinded types knocking about; our operations ! and &. Using type aliases we can push these together to define higher-kinded types with any number of arguments, such as:

type F[A, B, C] = ![A] & (B | C)

And, hey presto, we have a usable type-level representation for boolean functions already! Furthermore, we can think of our expressions as simply being type-level boolean functions with no arguments.

Tautologies

We’ll start with functions with one argument. def foo(a: Boolean):Boolean is a tautology only if foo(true) = true and foo(false) = true. So, for unary type-level functions, we define the tautology conditions simply as follows:

The expression we get when we fill in the argument with True must be true, and likewise for the expression we get when we fill in the argument with False.

Moving on to functions with two arguments; we now have 4 cases to check for def bar(a:Boolean, b:Boolean):Boolean. Luckily, when translating this to the type-level we’ve already done half the work! Notice that once we plug a value, for example true, into the first argument in bar , we’re left with a unary boolean function def faz(b: Boolean) = bar(true, b). Similarly, we can use UnaryTautology to define what it means for a type-level function with two arguments to be a tautology, as follows:

The unary function we get when we’ve filled in the first argument with True must be a tautology, and likewise when we’ve filled it in with False. We can continue this process of adding an argument at a time for as long as we would like (I went to three before thinking that was enough for my interest) and thus define what it means for a higher-kinded type to represent a tautology for any number of arguments! In this way, we check every single possible combination of boolean inputs to the function and whether the resulting expression is true. Here is the TertiaryTautology type-class, for completeness:

(Note 1: The only real limitation we have in this approach is the inability to represent a type that has an arbitrary number of type arguments. If we could do this, there would be no need to write out each progressively larger case by hand.)

We can now define tautology checking functions, and test them against our favourite logical laws:

Satisfiability

The first step is to notice that where for tautologies we needed to check the outputs of every single combination of inputs to the function, for satisfiability we only need to find one combination. This is the same as conducting a binary search over the input values, and that is what we will try and encode at the type-level. So, at each step we need something that will enact the search along the left-hand (True input) branch and something that does the same for the right-hand ( False input) branch. Naïvely, we might expect the first two layers to look like this:

However, this implementation is problematic. Consider trying to use these implicits in the following implementation:

def satisfiable2[E[_,_]](implicit s: BinarySatisfaction[E]) = ???

This will work just fine if the boolean function we are checking has exactly one set of inputs that satisfies the function, as the compiler will find exactly one implicit value that we can put in for s . But if our E has more than one set of inputs satisfying it (for example |[A,B], which is true when either, or both of its arguments are true) then the compiler will also find more than one implicit values that fit the bill, and the function satisfiable2 will not compile, with an ambiguous implicit values error. But, for satisfiability we really don’t care how many ways a function can be satisfied, just that it is satisfiable, so we have to force the compiler to stop looking as soon as it finds a correct series of implicits. In other words, we have to make the compiler perform a true binary search.

(Note 2: the above implementation provides a solution to the (unsurprisingly named) Unique Satisfiability Problem, so isn’t completely lacking in interest!)

As it happens, there is a pretty simple fix we can make to the above implementation to enforce this; using the compiler’s hierarchy of implicit search to give priority to the trueInput implicits, like so:

By making this change, we give sequences of inputs an ordering of priority. For two inputs, the following pairs of inputs are tested, one by one:

(True, True) > (True, False) > (False, True) > (False, False)

So, for example, take the binary boolean function XOR, that is true if and only if exactly one of its inputs is true. While both (True, False) and (False, True) fit the bill, the first has higher priority and will be the combination chosen by the compiler. Suppose we have written XOR as an Expression, and we try to compile satisfiable2[XOR]. The compiler will roughly do the following when searching for an implicit value of type BinarySatisfaction[XOR]:

  1. try using BinarySatisfaction.trueInput[XOR], which takes a value of type UnarySatisfaction[XOR[T, ?]].
  2. try using UnarySatisfaction.trueInput[XOR[T, ?]] to produce this value, which takes a value of type Truth[XOR[T, T]].
  3. Truth is well-defined, so the compiler won’t be able to find a value for Truth[XOR[T, T]] , so it will go to LowPriorityUnarySatisfaction and try to use the def falseInput[XOR[T, ?]] to produce this value, which takes a value of type Truth[XOR[T, F]].
  4. A value of type Truth[XOR[T, F]] exists (using the Truth implicits)! So the compiler found a value of type BinarySatisfaction[XOR] by going along the BinarySatisfaction.trueInput[XOR] path, and won’t even try using the lower priority BinarySatisfaction.falseInput[XOR] path.

As with tautologies we can continue to add more arguments by adding more type-classes. The one for tertiary functions would look like this:

And now we can define satisfiability functions that will actually work as we expect them to:

And there we go!

This project was in part inspired by work done in the library Numerology, which lifts a different set of mathematical operations to the type-level: arithmetic. If you want to check out the source code for this project, head over to TruthSerum.

The Startup

Get smarter at building your thing. Join The Startup’s +788K followers.

Thanks to James Phillips

Sign up for Top 10 Stories

By The Startup

Get smarter at building your thing. Subscribe to receive The Startup's top 10 most read stories — delivered straight into your inbox, once a week. Take a look.

By signing up, you will create a Medium account if you don’t already have one. Review our Privacy Policy for more information about our privacy practices.

Check your inbox
Medium sent you an email at to complete your subscription.

Jack Wheatley

Written by

Scala developer and proponent of functional programming

The Startup

Get smarter at building your thing. Follow to join The Startup’s +8 million monthly readers & +788K followers.

Jack Wheatley

Written by

Scala developer and proponent of functional programming

The Startup

Get smarter at building your thing. Follow to join The Startup’s +8 million monthly readers & +788K followers.

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store