The Boolean Blindness blog post by Dr. Robert Harper presents a generally excellent point: the use of Booleans is inherently connected with a loss of information, the so-called Boolean Blindness.
For example, even if we for some list
xs know that the expression
all even xs = True holds, we often can not use that information further along in our program1 and we still have to handle the cases where an element is odd, even though such case is impossible in practice.
Fortunately, as we will discuss in this post, it is possible to convert Boolean predicates to constructive predicates using a straightforward almost mechanical recipe. Let us take a simple example like calculating whether a natural number2 is even (or odd). We use an inductive definition which states that zero is even, one is not even, and adding two to any even number will result in an even number (ditto with odd numbers).
The process to convert the any Boolean predicate—including
even—to a type-level one is as follows:
We first create a data-type with the same signature as our function, except replacing each occurance of
True case, we create a new uniquely named constructor which is indexed by the functions patterns, and we replace any dependent calls to itself or other predicates with arguments that expect inhabitants of that call.
even example, the corresponding type-level predicate
Even will look as follows:
Another example is the less than or equal function
lte below. It follows a similar structure to our
even example, but this time also has multiple arguments; that is however not an issue since our presented technique generalises for any number of arguments.
Again we create a datatype with the required type signature, and map each
True case to a unique constructor, finally ending up with the type-level
For most type-level predicates that are converted from Boolean functions (namely those with decidable equality of arguments), it is usually possible to define decision procedures that allow users to regain the ability to decide whether the predicate holds. As can be seen below it follows the style of the Boolean functions, except that we have to be more careful around the branches where the predicate does not hold.
1: In most mainstream functional languages, like Haskell, Standard ML, F#, Racket, Scheme, etc.
2: Defined as
data Nat = Z | S Nat