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¹ 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² 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).

even : Nat -> Bool
even Z = True
even (S Z) = False
even (S (S n)) with (even n)
  even (S (S n)) | True = True
  even (S (S n)) | False = False

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:

data Even : Nat -> Type where
  Even_Z  : Even Z
  Even_SS : Even n -> Even (S (S n))

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.

lte : Nat -> Nat -> Bool
lte Z m = True
lte (S n) Z = False
lte (S n) (S m) with (n `lte` m)
  lte (S n) (S m) | True = True
  lte (S n) (S m) | False = False

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:

data Lte : Nat -> Nat -> Type where
  Lte_Z : Lte Z m
  Lte_S : Lte n m -> Lte (S n) (S m)

any : (a -> Bool) -> List a -> Bool
any f [] = False
any f (x :: xs) with (f x)
  any f (x :: xs) | True = True
  any f (x :: xs) | False with (any f xs)
  any f (x :: xs) | False | True = True
  any f (x :: xs) | False | False = False

data Any : (f : a -> Type) -> List a -> Type where
  Any_Here  : f x      -> Any f (x :: xs)
  Any_There : Any f xs -> Any f (x :: xs)

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.

notEven1 : Even 1 -> Void
notEven1 Even_Z impossible
notEven1 (Even_SS n) impossible

notEvenOff : (Even k -> Void) -> Even (S (S k)) -> Void
notEvenOff f (Even_SS x) = f x

decEven : (n : Nat) -> Dec (Even n)
decEven Z = Yes Even_Z
decEven (S Z) = No notEven1
decEven (S (S n)) with (decEven n)
  decEven (S (S n)) | (Yes prf) = Yes (Even_SS prf)
  decEven (S (S n)) | (No contra) = No (notEvenOff contra)

notLteZ : Lte (S k) 0 -> Void
notLteZ Lte_Z impossible
notLteZ (Lte_S l) impossible

notLteOff : (Lte n m -> Void) -> Lte (S n) (S m) -> Void
notLteOff f (Lte_S x) = f x

decLte : (n : Nat) -> (m : Nat) -> Dec (Lte n m)
decLte Z m = Yes Lte_Z
decLte (S n) Z = No notLteZ
decLte (S n) (S m) with (decLte n m)
  decLte (S n) (S m) | (Yes prf) = Yes (Lte_S prf)
  decLte (S n) (S m) | (No contra) = No (notLteOff contra)

notAnyEmpty : ((x : a) -> Dec (f x)) -> Any f [] -> Void
notAnyEmpty f (Any_Here x) impossible
notAnyEmpty f (Any_There xs) impossible

notAnyOff : (f x -> Void) -> (Any f xs -> Void) -> Any f (x :: xs) -> Void
notAnyOff notf notany (Any_Here x) = notf x
notAnyOff notf notany (Any_There x) = notany x

decAny : ((x : a) -> Dec (f x)) -> (xs : List a) -> Dec (Any f xs)
decAny decf [] = No (notAnyEmpty decf)
decAny decf (x :: xs) with (decf x)
  decAny decf (x :: xs) | (Yes prf) = Yes (Any_Here prf)
  decAny decf (x :: xs) | (No contra) with (decAny decf xs)
    decAny decf (x :: xs) | (No contra) | (Yes prf) = Yes (Any_There prf)
    decAny decf (x :: xs) | (No contra) | (No contra') =  No (notAnyOff contra contra')

1: In most mainstream functional languages, like Haskell, Standard ML, F#, Racket, Scheme, etc.

2: Defined as data Nat = Z | S Nat