## Introduction

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 program^{1} 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 number^{2} 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 `Bool`

with `Type`

.
For each `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.
For our `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 `Lte`

predicate:

## Decisions, Decisions

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`