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