"Booleans Considered Harmful Blog"

Written By Atticus Kuhn
Tags: "denotational", "design", "public", "blog", "project"
:PROPERTIES: :ID: 46904bc5-7ea9-41cb-9e53-60c5c9171b47 :mtime: 20230919150232 20230919134343 :ctime: 20230919134341 :END: #+title: Booleans Considered Harmful Blog #+filetags: :denotational design:public:blog:project: * Boolean Considered Harmful I make the claim that using the boolean type (called "Boolean") is always a bad design decesion. This is because `Boolean` is like the rind of an orange that has been squeezed out. The rind testifies that there once was an orange here, but the juicy goodness of the orange is long gone. It is the same with `Boolean`. If you are using `Boolean`, there was once a function which returned more information, but this helpful information was thrown away when all the information was squashed down into only 2 states. My recommendation is that for any time you are tempted to write "Boolean", consider what information the function is actually computing. To illustrate my point more, I will code the equality function on natural numbers in [[id:0f71a1c3-958b-4895-86b9-33d225a393ea][Agda]]. For any natural numbers `x` and `y`, `x = y` returns `true` if `x` is equal to `y` and false otherwise. I will then contrast this function against `x ==? y`, which I claim is a better function. Do not worry if you do not know [[id:0f71a1c3-958b-4895-86b9-33d225a393ea][Agda]], because I will be explaining the code at every step. * Standard Library Functions First, I will defining some standard functions. These functions are all in the [[id:b747d7e8-e5a7-4977-8656-b824d57f8de7][standard library of Agda]], so this section is a learning exercise where I will be thouroughly explaining the purpose of all the code. ** Peano Numbers We will represent natural numbers as [[id:5ea4fd4f-6fe8-4960-8f03-9a0f5cb1f665][Peano Numbers]], which means that every natural number is either `0` or `successor(n)` for some natural number `n`. In Agda, we would represent the natural numbers as this data type: #+BEGIN_SRC agda2 data NaturalNumber : Set where zero : NaturalNumber successor : NaturalNumber → NaturalNumber variable m n : NaturalNumber #+END_SRC ** Booleans We can then define the much-dreaded `Boolean`, which is either `true` or `false`. #+BEGIN_SRC agda2 data Boolean : Set where true : Boolean false : Boolean #+END_SRC ** Booleanean (Bad) Equality In our first attempt to define equality on natural numbers, we use a `Boolean` to represent the result: `true` if the two numbers are equal and `false` if the two numbers are not equal. #+BEGIN_SRC agda2 infixr 5 _==_ _==_ : NaturalNumber → NaturalNumber → Boolean zero == zero = true successor a == zero = false zero == successor b = false successor a == successor b = a == b #+END_SRC ** Propositional Equality To begin to define our better equality, we first need a specification of equality. Some beginners are confused by propositional equality because propositional equality does not *compute* if two values are equal, but rather it gives the type of all *proofs* that they are equal. #+BEGIN_SRC agda2 infixr 5 _≡_ data _≡_ {A : Set o} : A → A → Set (lsuc o) where reflexivity : {a : A} → a ≡ a #+END_SRC So, for example, `a ≡ b` is the type of all proofs that `a` is equal to `b`. ** Empty Type The empty type is inhabited by no values. The empty type represents the false proposition, or the proposition with no proofs. #+BEGIN_SRC agda2 data empty : Set where #+END_SRC ** Decidability With these pieces, we can define `decidability`. A proposition is [decidable](https://en.wikipedia.org/wiki/Decidability_(logic)) if there exists an algorithm for deciding if the proposition is inhabited. The `decides A` type will either produce evidence that `A` is inhabited, or produce evidence that `A` in uninhabited. #+BEGIN_SRC agda2 data decides (A : Set o) : Set o where trueBecauseOf : A → decides A falseBecauseOf : (A → empty) → decides A #+END_SRC A simple utility function which proves that `successor` is an [[id:99e654a7-b030-4e21-840a-be56ba8dc86f][injective function]]. #+BEGIN_SRC agda2 successorInjective : successor m ≡ successor n → m ≡ n successorInjective reflexivity = reflexivity #+END_SRC Given the type `decides`, we can say what it means for a [[id:18cec7be-7d44-46e5-986c-897fdc86d3df][Binary Operation]] to be decidable: for all its inputs, we can produce evidence of the type being inhabited or uninhabited. #+BEGIN_SRC agda2 decidable2 : {A B : Set o} → (A → B → Set ℓ) → Set (o ⊔ ℓ) decidable2 {A = A} {B = B} f = (a : A) (b : B) → decides (f a b) #+END_SRC * The Improved Natural Number Equality We will now define the improved equality function on natural numbers: #+BEGIN_SRC agda2 infixr 5 _==?_ _==?_ : decidable2 {A = NaturalNumber} (_≡_) zero ==? zero = trueBecauseOf reflexivity zero ==? successor y = falseBecauseOf λ () successor x ==? zero = falseBecauseOf λ () successor x ==? successor y with (x ==? y) ... | trueBecauseOf reflexivity = trueBecauseOf reflexivity ... | falseBecauseOf x≢y = falseBecauseOf (λ z → x≢y (successorInjective z)) #+END_SRC * Why the Deciding Verison is Better You might be wondering: "why is `x = y better than `x ==? y` ". In short, it is because `x ==? y` has a specification, but `x = y` does not. What's more, for all inputs, `x ==? y` returns evidence that it is correct, whereas we have not even stated the correctness specification for `x = y`. You should always assume that everything is wrong until you have a formal proof that it is correct. Any function with the type signature `decidable2 {A = NaturalNumber} (_≡_)` *must* be correct. By using a more expressive type, we have ensured correctness automatically. Others have said "[[id:fd1e50ac-0953-4358-af67-11b1d220d886][make illegal states unrepresentable]]" but I say, "make incorrect code unwritable". Write a specification so that the only option is for your code to be correct. With the pedestrian `x == y`, it would be easy to write a function with the same type signature that, in fact, would be incorrect. The main concern in software is proofs of correctness. Every other aspect of code (including performance) is secondary. To learn more about this, look at[[id:0132b0c6-b3b3-4aa8-a6cb-a140cfc9aeb1][A Galilean revolution for computing: Unboundedly scalable reliability and efficiency]]. For these reasons, I strongly advise that 90% of the use of `Boolean`s is incorrect, and could be replaced by more informative types.

See Also

AgdaAgdastandard library of AgdaPeano Numbersinjective functionBinary Operationmake illegal states unrepresentableA Galilean revolution for computing: Unboundedly scalable reliability and efficiency

Leave your Feedback in the Comments Section