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
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
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
corresponds to a given integer.
A solution to the second problem is to introduce a
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.
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.
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