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:
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
The Truth implicits are easy enough to reason through:
Truemust always be true, so it has an implicit defined
Falsemust never be true, so it doesn’t have an implicit
![E]is true only in the case where
E1 & E2is true only in the case where both
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
! 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
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:
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
&. 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.
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
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:
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 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
- try using
BinarySatisfaction.trueInput[XOR], which takes a value of type
- try using
UnarySatisfaction.trueInput[XOR[T, ?]]to produce this value, which takes a value of type
Truthis well-defined, so the compiler won’t be able to find a value for
Truth[XOR[T, T]], so it will go to
LowPriorityUnarySatisfactionand try to use the def
falseInput[XOR[T, ?]]to produce this value, which takes a value of type
- A value of type
Truth[XOR[T, F]]exists (using the
Truthimplicits)! 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
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!