# Boolean Logic Using the Scala Compiler

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

First, we will build our language of logical expressions. The type `Boolean`

has two instances: `true`

and `false`

, and so we are going to begin with two new types that will represent these instances:

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

Now that we have these building blocks in place, we can address our first goal: a function `def isTrue[E <: Expression]`

that compiles if and only if the logical expression that `E`

represents is true. We begin with two type classes representing the two possible evaluations:

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:

- left expression is false, right is true
- right expression is false, left is true
- 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

Now that we have managed to express what it means for an expression to be “true at compile-time”, we can turn to looking at boolean functions; functions from one or more boolean values to a single boolean value. In runtime-level code, this is something that looks like:

`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

With these observations in hand, we can start thinking about writing functions `def tautology[E[_,_]]`

that compiles if and only if the type `E`

represents a tautological function (in this case taking two arguments).

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

Now onto our second goal of this section; encoding satisfiability of boolean functions at the type-level. Remember, a boolean function is **satisfiable** if there exists some input values such that the output value is true. Like we had for tautologies, we’re going end up with a series of functions: `def satisfiable1[E[_]]`

, `def satisfiable2[E[_,_]]`

, etc., to account for the different function arities (also see **note 1** above!).

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]`

:

- try using
`BinarySatisfaction.trueInput[XOR]`

, which takes a value of type`UnarySatisfaction[XOR[T, ?]]`

. - try using
`UnarySatisfaction.trueInput[XOR[T, ?]]`

to produce this value, which takes a value of type`Truth[XOR[T, T]]`

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

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