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