## Boolean Blindness

I hate Booleans!  But isn’t everything “just bits”?  Aren’t computers built from gates?  And aren’t gates just the logical connectives?  How can a Computer Scientist possibly hate Booleans?

Fritz Henglein recently pointed out to me that the world of theoretical Computer Science is divided into two camps, which I’ll call the logicians (who are concerned with languages and semantics) and the combinatorialists (who are concerned with algorithms and complexity).  The logicians love to prove that programs work properly, the combinatorialists love to count how many steps a program takes to run.  Yet, curiously, the logicians hate the Booleans, and love abstractions such as trees or streams, whereas the combinatorialists love bits, and hate abstraction!  (Or so it often seems; allow me my rhetorical devices.)

My point is this.  Booleans are just one, singularly (or, perhaps, binarily) boring, type of data.  A Boolean, b, is either true, or false; that’s it.  There is no information carried by a Boolean beyond its value, and that’s the rub.  As Conor McBride puts it, to make use of a Boolean you have to know its provenance so that you can know what it means.

Booleans are almost invariably (in the CS literature and textbooks) confused with propositions, which express an assertion, or make a claim.  For a proposition, p, to be true means that it has a proof; there is a communicable, rational argument for why p is the case.  For a proposition, p, to be false means that it has a refutation; there is a counterexample that shows why p is not the case.

The language here is delicate.  The judgement that a proposition, p, is true is not the same as saying that p is equal to true, nor is the judgement that p is false the same as saying that p is equal to false!  In fact, it makes no sense to even ask the question, is p equal to true, for the former is a proposition (assertion), whereas the latter is a Boolean (data value); they are of different type.

In classical mathematics, where computability is not a concern, it is possible to conflate the notions of Booleans and propositions, so that there are only two propositions in the world, true and false.  The role of a proof is to show that a given proposition is (equal to) one of these two cases.  This is well and good, provided that you’re not interested in computing whether something is true or false.  As soon as you are, you must own up to a distinction between a general proposition, whose truth cannot be decided, and a Boolean, which can be computed one way or the other.  But then, as was mentioned earlier, we must link it up with a proposition expressing what the Boolean means, which is to specify its provenance.  And as soon as we do that, we realize that Booleans have no special status, and are usually a poor choice of data structure anyway because they lead to a condition that Dan Licata calls Boolean blindness.

A good example is the equality test, e=e’, of type bool.  As previously discussed, this seemingly innocent function presents serious complications, particularly in abstract languages with a rich type structure.  It also illustrates the standard confusion between a proposition and a Boolean.  As the type suggests, the equality test operation is a function that returns either true or false, according to whether its arguments are equal or not (in a sense determined by their type).  Although the notation invites confusion, the expression e=e’ is not a proposition stating that e and e’ are equal!  It is, rather, a piece of data of one of two forms, either true or false.  The equality test is a function that happens to have the property that if it returns true, then its arguments are equal (an associated equality proposition is true), and if it returns false, then its arguments are not equal (an associated equality proposition is false), and, moreover, is ensured to return either true or false for any inputs.  This may seem like a hair-splitting distinction, but it is not!  For consider, first of all, that the equality test may have been written with a different syntax, maybe e==e’, or (equal? e e’), or any number of other notations.  This makes clear, I hope, that the connection between the function and the associated proposition must be explicitly made by some other means; the function and the proposition are different things.  More interestingly, the same functionality can be expressed different ways.  For example, for partially ordered types we may write e<=e’ andalso e'<=e, or similar, satisfying the same specification as the innocent little “equals sign” function.  The connection is looser still here, and still looser in numerous other variations that you can spin for yourself.

What harm is there in making this confusion?  Perhaps the greatest harm is that it confuses a fundamental distinction, and this has all sorts of bad consequences.  For example, a student may reasonably ask, why is equality not defined for functions?  After all, in the proof I did the other day, I gave a carefully argument by structural induction that two functions are equal.  And then I turn around and claim that equality is not defined for functions!  What on earth am I talking about?  Well, if you draw the appropriate distinction, there is no issue.  Of course there is a well-defined concept of two functions being mathematically equal; it, in general, requires proof.  But there is no well-defined computable function that returns true iff two functions (on integers, say) are equal, and false otherwise.  Thus, = : (int->int) x (int->int) -> prop expresses equality, but = : (int->int)->(int->int)->bool cannot satisfy the specification just given.  Or, to put it another way, you cannot test equality of propositions!  (And rightly so.)

Another harm is the condition of Boolean blindness alluded to earlier.  Suppose that I evaluate the expression e=e’ to test whether e and e’ are equal.  I have in my hand a bit.  The bit itself has no intrinsic meaning; I must associate a provenance with that bit in order to give it meaning.  “This bit being true means that e and e’ are equal, whereas this other bit being false means that some other two expressions are not equal.”  Keeping track of this information (or attempting to recover it using any number of program analysis techniques) is notoriously difficult.  The only thing you can do with a bit is to branch on it, and pretty soon you’re lost in a thicket of if-the-else’s, and you lose track of what’s what.  Evolve the program a little, and you’re soon out to sea, and find yourself in need of sat solvers to figure out what the hell is going on.

But this is yet another example of an iatrogenic disorder!  The problem is computing the bit in the first place.  Having done so, you have blinded yourself by reducing the information you have at hand to a bit, and then trying to recover that information later by remembering the provenance of that bit.  An illustrative example was considered in my article on equality:

fun plus x y = if x=Z then y else S(plus (pred x) y)

Here we’ve crushed the information we have about x down to one bit, then branched on it, then were forced to recover the information we lost to justify the call to pred, which typically cannot recover the fact that its argument is non-zero and must check for it to be sure.  What a mess!  Instead, we should write

fun plus x y = case x of Z => y | S(x’) => S(plus x’ y).

No Boolean necessary, and the code is improved as well!  In particular, we obtain the predecessor en passant, and have no need to keep track of the provenance of any bit.

[Update: removed last paragraph.]

### 27 Responses to Boolean Blindness

1. danielbrice says:

Interestingly, the world of research Mathematics is also divided into two camp: the “theory builders” and the “problem solvers”. The theory builders (analogous to your logicians) are concerned with establishing the right foundational framing for a subject area in such a way that all interesting established results end up trivially following from the base axioms of the subject. The problem solvers (analogous to your combinatorialists) are there to provide those interesting established results that the theory builders strive to find footing for, and then to work out the rest of the results by hand when the theory builders inevitably fail to make all interesting results trivial :-p

It’s actually a very fruitful tug of war, resulting in more and richer theories and ever deeper results.

Like

2. […] I recommend Bob Harper’s essay on “boolean blindness”: https://existentialtype.wordpress.com/2011/03/15/boolean-bli&#8230; […]

Like

3. […] From here (blog post by Robert Harper, his advisor at CMU): […]

Like

4. You might be interested to know that in the Aha! programming language, designed by me, the Boolean data type is just missing. Although anyone can define it if needed, no language construct relies on the existence of Boolean. You can have a look at my website to find out more, the entire language may become a revelation to many!

Like

5. johneganz says:

When dealing with “computers”, at least their physical manifestations and not some abstract mathematical idea, there is exactly one type, a boolean bit, and exactly one operation: NAND (Not AND). For those unfamiliar with this principle, I suggest the wikipedia article on NAND logic.

There is nothing else. Everything decomposes to this one type and one operation. For those that doubt this, the Apollo Guidance Computer was built with exactly one type of gate: a 3 input NOR gate, and the Cray-1 supercomputer was built using just four different IC’s- two of them were memory chips, while the logic for the computer was implemented using two IC’s that both implemented a dual 5 / 4 input NOR gate.

No Boolean necessary, and the code is improved as well! In particular, we obtain the predecessor en passant, and have no need to keep track of the provenance of any bit.

No, you haven’t. All you have done is heaped so much syntactic sugar on this mess that you have forgotten that all that sugar is just an abstraction. In fact, your “cleaner” example just decomposes to the “uglier” previous example when you strip away the sugar. So what, exactly, have you gained?

Don’t get me wrong- I’m all for syntactic sugar that makes people more productive.

But what you’re trying to do is claim that your particular shade of syntactic sugar is somehow better than everyone elses.

What’s worst is that for the first half of your post, you argue that booleans are completely unsuitable for computation, and how abstract concepts from mathematics do not reduce cleanly to booleans.

Except… here’s the problem. Are we talking about computers? “Computation” (in so far as what one does with physically realized computers)? Then we are talking about systems that are built from exactly one type- a boolean bit, and one operation- NAND. Anything that can’t be reduced to this is outside the domain of computation, at least from a practical and pragmatic sense as it exists today.

The problems that you “perceive” have nothing to do with the problems of computers, computation, or languages. The problem is you are pounding square pegs in to round holes, and you don’t even realize it.

As an exercise, convince yourself that the entire business of “null pointer analysis” is pointless, for exactly the same reasons! There are few things more stupid in the world than code that compares a pointer for equality with null, then branches on the outcome, and then finds itself needing a sat solver or model checker to propagate the provenance of a boolean that should never have been computed in the first place!

…whistle… I can only imagine what the view must be like from that ivory tower.

Like

• “Except… here’s the problem. Are we talking about computers?”

No!! We absolutely are not talking about computers. We’re talking about computation, which is much, much more general than “what one does with physically realized computers”.

“[Computer science] is not really about computers — and it’s not about computers in the same sense that physics is not really about particle accelerators, and biology is not about microscopes and Petri dishes…and geometry isn’t really about using surveying instruments.” — Hal Abelson

Like

• sambocyn says:

yeah well see after I read this article I re-factored a Bool into a Maybe, and the call stack of functions that felt wrong became easier to think about. no “ivory”.

Like

• Cool!

Like

6. johnzabroski says:

Andreas,

You are right, and so is Bob. But Bob misses out on slamming the mother of all poorly designed libraries – and it is also the most widely used library in programming history: jQuery.

Bob,

jQuery epitomizes what is wrong with programming today, and your blog post exemplifies why.

What does it say about programming that most programmers find jQuery easy to use? What does it say about programming that jQuery is very hard to actually maintain?

Like

• abstract type says:

I don’t know enough about JQuery to comment. Maybe you could fill us in?

Like

• johnzabroski says:

Best reference would be Garritt Smith’s JavaScript Query Engines article from DHTML Kitchen dot com (and the associated links off that article). Beware: This article and the associated links lead back to news://comp.lang.javascript, which is basically a shouting ground for people forced to use JavaScript and deal with other “JavaScript programmers” bad code – the language and attitudes on that discussion forum can get pretty rough!

Note that an actor-based solution would be better than what most JavaScript libraries currently do, since actors do not allow separating data flow from control flow; the only way you are allowed to share data is through message passing. (JavaScript itself is actually well-situated for event-loop concurrency, since there are no threads in the language.) Similarly, I believe Concurrent Prolog would be the earliest example of what you personally are after, since all communication is handled through built-in primitives (e.g., there is no special status for program-to-file, process-to-process, etc. forms of communication).

By the way, it is unfortunate you reference a student of yours (Dan Licata) and imply that he was the first to rail against Boolean Blindness. While I imagine Dan is very bright, he is also missing his whiskers. To the best of my knowledge, Ted Codd was the first to point out, in his relational model, that there is no place for Boolean data types in entity modeling. It is a basic design principle to avoid characterizing data in terms of Boolean values, since there is usually some other piece of information you are forgetting to model, and once you slam a Boolean into your overall data model, it becomes very hard to version towards a more exact model (information loss). I prefer Codd’s view to the explanation you give here, but they are complementary! CJ Date has updated this explanation in many of his textbooks (the Third Manifesto itself is about creating a query language based on predicate logic rather than sets/bags). In particular, for what Andreas refers to, CJ Date and Hugh Darwen call it The First Great Blunder of DBMS implementors.

Like

• abstract type says:

Thanks for the Codd reference, I’ll check that out. My attribution to Dan pertains to our class; this is the formulation he came up with when teaching about this issue this semester.

Like

7. I kind of see your point, but I don’t understand why you seem to think that your observation is specific to Booleans. For example, how do the 1.58 bits of information embodied in ML’s “order” type carry any more context? How does a bare natural number include context about what it is counting? Would you also argue against – excuse the pun – Natural Blindness? (Arguably, physicists have invented units of measure to cope to some extent. But despite Andrew’s nice work, they haven’t caught on in computing.)

An equivalent problem seems to occur whenever we have some more complex datum d and extract/abstract some simpler property p from it, be it a bit, the sign of a number, the ordering relation between a pair of numbers, the length of a list, etc. This is fine as long as p is all we need to go along. But if we actually go on manipulating d based on p, then we are relying on a relation between the two that is entirely implicit in the program. (I noticed that you were writing “if |list| = 0 then …” to express quicksort in a later post, which already composes two instances of this very approach.)

Something like views (however realized), refinement types, or other forms of dependent types might help in a lot of cases, I guess, but are they a general answer? Can we even hope to solve the problem more generally?

Like

• abstract type says:

It’s just that Boolean thinking has infected the software world to such an extent that I feel that I have to fight back. Just the idea of comparison to “null” to obtain a Boolean is absurd, even if you think you need a “null” pointer (which you don’t, in a properly designed language).

Like

8. johnwcowan says:

Conflating truth and provability means that some truthful statements aren’t propositions at all. But if not, what are they?

Like

• abstract type says:

I don’t understand this question at all.

Like

9. steven807 says:

Interesting! I’ve been programming in Erlang for a few years, and “if” is a second-class citizen — generally more awkward to use than “case”. I’ve noted that, once I get used to the language, I just about never want to use “if”, but I never had a clear sense why. Your explanation makes sense: a single bit of information is pretty boring, when there are so many other, richer ways of deconstructing data!

-Steven

Like

• abstract type says:

Glad to hear it. Pattern matching is extremely useful for both development and maintenance of code.

Like

10. dannysleator says:

My apologies for the messed up indentation in my previous comment. I stupidly assumed that the “code” html tags would respect blanks. Silly me.

Like

• abstract type says:

Here there’s not much you can do, but there are plenty of cases where you can, and therefore should, avoid Booleans. This is especially true for teaching beginners. It’s just dreadful the way they end of in rat’s nests of conditional branches completely unnecessarily, all because they think they should reduce every condition to a Boolean, then branch on it.

Like

11. dannysleator says:

I don’t really understand, from an operational perspective (i.e. as a working programmer) what this means. For example, here’s a little program I wrote in ocaml that computes the next prime up from an integer that I give it. It makes heavy use of booleans (constants true and false as well as boolean expressions). I would you write this?

``` let next_prime_up n = let isprime n = let rec loop i = if (i*i > n) then true else if n mod i = 0 then false else loop (i+2) in loop 3 in let rec search i = if isprime i then i else search (i+2) in if n<2 then 2 else if n=2 then 3 else search ((n+1) lor 1) ```

Like

• yminsky says:

I’ve run into some of the same issues described above with respect to bools. I don’t think there’s anything wrong with bools per se, but you have to be careful to keep the context clear. The same thing is true to only a somewhat lesser degree for integers! I think this is a general problem with types that have broad applicability and that are thus not tied into the specific meaning of your program.

Your code above seems unobjectionable to me. The problems arise when boolean values are moved around without sufficient contextual clues. I find OCaml’s labeled arguments to be an effective way of making sure the context is clear across function calls.

Like

• Dan Doel says:

The answer is: you need a better language. :)

For instance, isprime shouldn’t be returning a boolean, it should be returning either a proof that its argument is prime, or a proof that some smaller number divides it. Most of the other tests can be modified in the same way (i*i > n for instance can be turned into a decision procedure for a similar looking proposition at the least).

If you keep the specification of next_prime_up, then you’d end up throwing away most of this extra information. But you could also elect to produce both the value and a proof that it really is the lowest prime greater than or equal to its argument.

For a simpler example, in Agda, one might make filter look like:

`filter : (A : Set) -> (P : A -> Set) -> (dec : (x : A) -> P x \/ Not (P x)) -> List A -> Exists (List A) (All P)`

which doesn’t just filter the list by a boolean function, but uses a decidable predicate, and returns a list, together with a proof that everything in the list satisfies the predicate.

Of course, the practicality of this approach is currently not so great (less fundamentally and more in implementation realities), but it’s getting better, and may eventually just be the way things are done.

Like

• sambocyn says:

maybe the author would say that {isprime} and {(<k)} should return {Maybe Int} not {Bool}?

Like

• It’s hard to make a blanket statement, but in the sense of this post, yes. I see this as akin to the much more sophisticated ideas of Kurt Mehlhorn on building certifying algorithms. For example, according to his proposal, a planarity tester should not take a graph and return boolean. Instead, it should take a graph and return either (a) an embedding of it into the plane, or (b) an embedding of either of the two Kuratowski sub-graphs into it, proving that it is non-planar. One motivation is it enables one to check the validity of the result; another might be that the additional information is what is really required by an application that wishes to perform planarity testing. Whether this is so is context-dependent, but one can imagine contexts in which that is helpful.

Like

12. […] that help manage the mess we’ve created—tools that do things like recover from Boolean blindness or check for null pointer errors.  To be sure, these tools are totally amazing, but then so are […]

Like

• I don’t see how (Set,Bool) (or Bool with a phantom type argument) doesn’t work just as well. Personally, I think that Bool is a *better* representation than Equality because you don’t have to lie to your language if you want to lie to your program and you can rely on external code for equality (and you could probably also lie to your language here).

Like