# Overcoming Boolean blindness with Evidence

Boolean blindness has been discussed over and over and over and over again. The conclusion seems to be that always using Boolean values for decisions is a generally bad idea and that using church encoded lambda calculus instead is not much better (and impractical). Here are my two cents on the matter: Use evidence instead of Boolean values.

For the purpose of this post I will use a contrived example. It is important to focus on the problem of boolean blindness here, and not the efficiency of the solution to the given problem.

### Boolean blindness for primes

Say you want to implement a primality test. You might write a function with the following signature:

`isPrime :: Int -> Bool`

The first problem with this function is the way it will be used. The call site of this function needs to know that the Boolean value it obtains reflects on the primality of the integer. This phenomenon is called Boolean blindness.

The second problem is that we have to trust that `isPrime`

works and the only way to check that the resulting Boolean corresponds to a
given integer is by evaluating `isPrime`

again. In other words:
There is no way to link the resulting Boolean value back to the integer under
test other than to ‘remember’ where it came from.

### Another name for the Boolean value

The first proposed solution consists of introducing a type isomorphic to
`Bool`

with a more meaningful name and more meaningful
constructors:

```
data Primality
= IsPrime
| NotPrime
isPrime :: Int -> Primality
```

This solves the Boolean blindness problem, but we still have to evaluate
`isPrime`

again to check that a given `Primality`

value
corresponds to a given integer.

### Evidence

A solution to the second problem is to introduce a `newtype`

`Prime`

and write a smart constructor for it:

```
newtype Prime = Prime Int -- INVARIANT: must be prime
prime :: Int -> Maybe Prime
```

Now you can rigorously test that any value produced by this
`prime`

function does in fact contain a prime. Then a
`Prime`

value can serve as evidence that the value within is
prime. In this way we can relate a `Prime`

value back to the
integer it concerns and we have solved the Boolean blindness problem.

### Testing

I use the word ‘evidence’ because I really mean ‘evidence’. In a perfect world we would use a proof, but unfortunately here we have to resort to evidence.

The power of the evidence comes from the testing we use to ensure that the invariants hold at all times.

With the validity and genvalidity libraries, you could write the following:

```
instance Validity Prime where
isValid = -- primality test here
instance GenValidity Prime where
genUnchecked = Prime <$> arbitrary
```

The tests are then simple to write with genvalidity-hspec:

```
primeSpec :: Spec
primeSpec = do
describe "Prime" $ do
validitySpec (Proxy :: Proxy Prime)
describe "prime" $ do
it "only produces valid primes"
validIfSucceedsOnArbitrary prime
```