Booleans

Posted on 2014-04-01 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Booleans
  ( Boolean, true, false, ifThenElse, isTrue, isFalse
  , _test_boolean, main_boolean
  ) where

import Testing
import Functions
import Flip
import Clone
import Composition

Before we think about numbers or writing programs, let’s start by nailing down some important ideas about truth values. In math there can be a kind of other-worldness about true and false, since they live in the “metalanguage” of mathematical logic rather than the “object language” of whatever we are studying. But it will turn out to be useful to algebraify the truth values themselves.

We’re going to characterize the boolean values true and false in a roundabout way. First, we define a kind of algebra.

A doubly-pointed set is a set \(A\) with two (not necessarily distinct) distinguished elements \(a_t, a_f \in A\). If \(A\) and \(B\) are doubly-pointed sets with distinguished elements \(a_t, a_f \in A\) and \(b_t, b_f \in B\), a map \(\theta : A \rightarrow B\) is called a doubly-pointed homomorphism if \(\theta(a_t) = b_t\) and \(\theta(a_f) = b_f\).

As algebras go, doubly-pointed sets are almost as weak as they come. We can see shades of the boolean values there – “true” and “false” can be thought of as distinguished elements in a doubly-pointed set. And indeed we’ll do that. But the booleans are not just any doubly-pointed set; they are the smallest such set in a precise sense.

There is a special doubly-pointed set, denoted \(\bool\), with distinguished elements \(\btrue\) and \(\bfalse\), with the property that if \(A\) is a doubly-pointed set with distinguished elements \(a_t, a_f\), then there is a unique doubly-pointed homomorphism \(\Theta : \bool \rightarrow A\). We denote this \(\Theta\) by \[\Theta(p) = \bif{p}{a_t}{a_f}.\]

What makes the booleans special among doubly-pointed sets is this unique map, which looks suspiciously like the traditional “if-then-else” construct, because that’s exactly what it is.

Let \((A,a_t,a_f)\) be a doubly pointed set. Then we have the following.

\(\bif{\btrue}{a_t}{a_f} = a_t\).
\(\bif{\bfalse}{a_t}{a_f} = a_f\).

_test_if_true :: (Boolean b, Equal a)
  => b -> a -> Test (a -> a -> Bool)
_test_if_true p _ =
  testName "if(true,a,b) == a" $
  \x y -> eq (ifThenElse (true `withTypeOf` p) x y) x


_test_if_false :: (Boolean b, Equal a)
  => b -> a -> Test (a -> a -> Bool)
_test_if_false p _ =
  testName "if(false,a,b) == a" $
  \x y -> eq (ifThenElse (false `withTypeOf` p) x y) y

This is a weird way to define \(\bool\) – but there’s a really good reason for it, which we’ll get into later.

I’m referring to “the” booleans as if they are uniquely determined, but of course they aren’t – any other doubly-pointed set that also maps uniquely to any other is indistinguishable from \(\bool\) up to a renaming of the special elements. For this reason we’ll wrap up the important information about \(\bool\) in a type class, rather than a single type.

class Boolean b where
  true, false :: b

  ifThenElse :: b -> a -> a -> a

Of course the Haskell Bool type is an instance.

instance Boolean Bool where
  true = True
  false = False

  ifThenElse p x y = if p then x else y

It will be handy later to name these two functions from an abstract boolean set to Bool.

isTrue :: (Boolean b) => b -> Bool
isTrue p = ifThenElse p true false

isFalse :: (Boolean b) => b -> Bool
isFalse p = ifThenElse p false true

There are many other instances which differ only by the labels of \(\btrue\) and \(\bfalse\), and depending on the context, a different concrete instance might make more sense. We could call the distinguished elements of \(\bool\) “Yes/No”, “Present/Absent”, or something else, and the essence of booleanness would not change.

\(\bif{\ast}{\ast}{\ast}\) enjoys some other nice properties. For instance, \(\bif{p}{a}{a} = \btrue\).

Let \(A\) be a set with \(a \in A\). If \(p \in \bool\), we have \[\bif{p}{a}{a} = a.\]

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bif{p}{a}{a} \\ & \let{p = \btrue} = & \bif{\btrue}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \end{eqnarray*}\] and if \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bif{p}{a}{a} \\ & \let{p = \bfalse} = & \bif{\bfalse}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & a \end{eqnarray*}\]

_test_if_same :: (Equal a, Boolean b)
  => b -> a -> Test (b -> a -> Bool)
_test_if_same _ _ =
  testName "if(p,a,a) == a" $
  \p a -> eq (ifThenElse p a a) a

\(\bif{\ast}{\ast}{\ast}\) interacts with function application.

Let \(A\) and \(B\) be sets with \(f : A \rightarrow B\) a map. For all \(p \in \bool\) and \(u,v \in A\), we have \[f(\bif{p}{u}{v}) = \bif{p}{f(u)}{f(v)}.\]

If \(p = \btrue\), we have \[\begin{eqnarray*} & & f(\bif{p}{u}{v}) \\ & \let{p = \btrue} = & f(\bif{\btrue}{u}{v}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & f(u) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{f(u)}{f(v)} \\ & \let{p = \btrue} = & \bif{p}{f(u)}{f(v)} \end{eqnarray*}\] as claimed. If \(p = \bfalse\), we have \[\begin{eqnarray*} & & f(\bif{p}{u}{v}) \\ & \let{p = \bfalse} = & f(\bif{\bfalse}{u}{v}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & f(v) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{f(u)}{f(v)} \\ & \let{p = \bfalse} = & \bif{p}{f(u)}{f(v)} \end{eqnarray*}\] as claimed.

_test_if_func :: (Equal a, Boolean b)
  => b -> a -> Test ((a -> a) -> b -> a -> a -> Bool)
_test_if_func _ _ =
  testName "f(if(p,a,b)) == if(p,f(a),f(b))" $
  \f p a b -> eq (f (ifThenElse p a b)) (ifThenElse p (f a) (f b))

Nested \(\bif{\ast}{\ast}{\ast}\)s commute (sort of).

Let \(A\) be a set with \(p,q \in \bool\) and \(a,b,c,d \in A\). Then we have \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & = & \bif{q}{\bif{p}{a}{c}}{\bif{p}{b}{d}}. \end{eqnarray*}\]

We have four possibilities for \((p,q)\). If \(p = \btrue\) and \(q = \btrue\), \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{p = \btrue} = & \bif{\btrue}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{q = \btrue} = & \bif{\btrue}{\bif{\btrue}{a}{b}}{\bif{\btrue}{c}{d}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{a}{c} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{\bif{\btrue}{a}{c}}{\bif{\btrue}{b}{d}} \\ & \let{p = \btrue} = & \bif{\btrue}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \\ & \let{q = \btrue} = & \bif{q}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \end{eqnarray*}\] as claimed. If \(p = \btrue\) and \(q = \bfalse\), \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{p = \btrue} = & \bif{\btrue}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{q = \bfalse} = & \bif{\btrue}{\bif{\bfalse}{a}{b}}{\bif{\bfalse}{c}{d}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\bfalse}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{b}{d} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\bif{\btrue}{a}{c}}{\bif{\btrue}{b}{d}} \\ & \let{q = \bfalse} = & \bif{q}{\bif{\btrue}{a}{c}}{\bif{\btrue}{b}{d}} \\ & \let{p = \btrue} = & \bif{q}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \end{eqnarray*}\] as claimed. If \(p = \bfalse\) and \(q = \btrue\), \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{p = \bfalse} = & \bif{\bfalse}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{q = \btrue} = & \bif{\bfalse}{\bif{\btrue}{a}{b}}{\bif{\btrue}{c}{d}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\btrue}{c}{d} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & c \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{c} \\ & \let{p = \bfalse} = & \bif{p}{a}{c} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \\ & \let{q = \btrue} = & \bif{q}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \end{eqnarray*}\] as claimed. If \(p = \bfalse\) and \(q = \bfalse\), \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \let{p = \bfalse} = & \bif{\bfalse}{\bif{q}{a}{b}}{\bif{q}{c}{d}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{q}{c}{d} \\ & \let{q = \bfalse} = & \bif{\bfalse}{c}{d} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & d \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{b}{d} \\ & \let{p = \bfalse} = & \bif{p}{b}{d} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \\ & \let{q = \bfalse} = & \bif{q}{\bif{p}{a}{c}}{\bif{p}{b}{d}} \end{eqnarray*}\] as claimed.

_test_if_nest :: (Boolean b, Equal a)
  => b -> a -> Test (Bool -> Bool -> a -> a -> a -> a -> Bool)
_test_if_nest _ _ =
  testName "if(p,if(q,a,b),if(q,c,d)) == if(q,if(p,a,c),if(p,b,d))" $
  \p q a b c d ->
    eq
      (ifThenElse p (ifThenElse q a b) (ifThenElse q c d))
      (ifThenElse q (ifThenElse p a c) (ifThenElse p b d))

Nested ifs on the same boolean can be pruned.

Let \(A\) be a set with \(p \in \bool\) and \(a,b,c \in A\). We have the following.

\(\bif{p}{\bif{p}{a}{b}}{c} = \bif{p}{a}{c}\)
\(\bif{p}{a}{\bif{p}{b}{c}} = \bif{p}{a}{c}\)

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bif{p}{\bif{p}{a}{b}}{c} \\ & \let{p = \btrue} = & \bif{\btrue}{\bif{\btrue}{a}{b}}{c} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{a}{c} \\ & \let{p = \btrue} = & \bif{p}{a}{c} \end{eqnarray*}\] as needed. If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bif{p}{\bif{p}{a}{b}}{c} \\ & \let{p = \bfalse} = & \bif{\bfalse}{\bif{\bfalse}{a}{b}}{c} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & c \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{c} \\ & \let{p = \bfalse} = & \bif{p}{a}{c} \end{eqnarray*}\] as needed.
If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bif{p}{a}{\bif{p}{b}{c}} \\ & \let{p = \btrue} = & \bif{\btrue}{a}{\bif{\btrue}{b}{c}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{a}{c} \\ & \let{p = \btrue} = & \bif{p}{a}{c} \end{eqnarray*}\] as claimed, and if \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bif{p}{a}{\bif{p}{b}{c}} \\ & \let{p = \bfalse} = & \bif{\bfalse}{a}{\bif{\bfalse}{b}{c}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{c} \\ & \let{p = \bfalse} = & \bif{p}{a}{c} \end{eqnarray*}\] as claimed.

_test_if_prune_left :: (Boolean b, Equal a)
  => b -> a -> Test (Bool -> a -> a -> a -> Bool)
_test_if_prune_left _ _ =
  testName "if(p,if(p,a,b),c) == if(p,a,c)" $
  \p a b c -> eq (ifThenElse p (ifThenElse p a b) c) (ifThenElse p a c)


_test_if_prune_right :: (Boolean b, Equal a)
  => b -> a -> Test (Bool -> a -> a -> a -> Bool)
_test_if_prune_right _ _ =
  testName "if(p,a,if(p,b,c)) == if(p,a,c)" $
  \p a b c -> eq (ifThenElse p a (ifThenElse p b c)) (ifThenElse p a c)

\(\bif{\ast}{\ast}{\ast}\) is sort of commutative.

Let \(A\) be a set. For all \(p,q \in \bool\) and \(a,b \in A\), we have the following.

\(\bif{p}{a}{\bif{q}{a}{b}} = \bif{q}{a}{\bif{p}{a}{b}}\)
\(\bif{p}{\bif{q}{a}{b}}{b} = \bif{q}{\bif{p}{a}{b}}{b}\)

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bif{p}{a}{\bif{q}{a}{b}} \\ & \let{p = \btrue} = & \bif{\btrue}{a}{\bif{q}{a}{b}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bif{q}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{q}{a}{\bif{\btrue}{a}{c}} \\ & \let{p = \btrue} = & \bif{q}{a}{\bif{p}{a}{c}} \end{eqnarray*}\] as claimed. If \(q = \btrue\), we have \[\begin{eqnarray*} & & \bif{q}{a}{\bif{p}{a}{b}} \\ & \let{q = \btrue} = & \bif{\btrue}{a}{\bif{p}{a}{b}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bif{p}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{p}{a}{\bif{\btrue}{a}{c}} \\ & \let{q = \btrue} = & \bif{p}{a}{\bif{q}{a}{c}} \end{eqnarray*}\] as claimed. Suppose then that \(p = q = \bfalse\); now \[\begin{eqnarray*} & & \bif{p}{a}{\bif{q}{a}{b}} \\ & \let{p = \bfalse} = & \bif{\bfalse}{a}{\bif{q}{a}{b}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{q}{a}{b} \\ & \let{q = \bfalse} = & \bif{\bfalse}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{b} \\ & \let{p = \bfalse} = & \bif{p}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{\bif{p}{a}{b}} \\ & \let{q = \bfalse} = & \bif{q}{a}{\bif{p}{a}{b}} \end{eqnarray*}\] as claimed.
If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{b} \\ & \let{p = \bfalse} = & \bif{\bfalse}{\bif{q}{a}{b}}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bif{q}{b}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{q}{\bif{\bfalse}{a}{b}}{b} \\ & \let{p = \bfalse} = & \bif{q}{\bif{p}{a}{b}}{b} \end{eqnarray*}\] as claimed. If \(q = \bfalse\), we have \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{b} \\ & \let{q = \bfalse} = & \bif{p}{\bif{\bfalse}{a}{b}}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{p}{b}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\bif{p}{a}{b}}{b} \\ & \let{q = \bfalse} = & \bif{q}{\bif{p}{a}{b}}{b} \end{eqnarray*}\] as claimed. If \(p = q = \btrue\), we have \[\begin{eqnarray*} & & \bif{p}{\bif{q}{a}{b}}{b} \\ & \let{q = \btrue} = & \bif{p}{\bif{\btrue}{a}{b}}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{p}{a}{b} \\ & \let{p = \btrue} = & \bif{\btrue}{a}{b} \\ & \let{q = \btrue} = & \bif{q}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{q}{\bif{\btrue}{a}{b}}{b} \\ & \let{p = \btrue} = & \bif{q}{\bif{p}{a}{b}}{b} \end{eqnarray*}\] as claimed.

_test_if_commute_left :: (Equal a, Boolean b)
  => b -> a -> Test (Bool -> Bool -> a -> a -> Bool)
_test_if_commute_left _ _ =
  testName "if(p,a,if(q,a,b)) == if(q,a,if(p,a,b))" $
  \p q a b -> eq
    (ifThenElse p a (ifThenElse q a b))
    (ifThenElse q a (ifThenElse p a b))

_test_if_commute_right :: (Equal a, Boolean b)
  => b -> a -> Test (Bool -> Bool -> a -> a -> Bool)
_test_if_commute_right _ _ =
  testName "if(p,if(q,a,b),b) == if(q,if(p,a,b),b)" $
  \p q a b -> eq
    (ifThenElse p (ifThenElse q a b) b)
    (ifThenElse q (ifThenElse p a b) b)

\(\bif{\ast}{\ast}{\ast}\) interacts with functions of two arguments.

We have \[f(\bif{p}{a}{c},\bif{p}{b}{d}) = \bif{p}{f(a,b)}{f(c,d)}.\]

If \(p = \btrue\), we have \[\begin{eqnarray*} & & f(\bif{p}{a}{c},\bif{p}{b}{d}) \\ & \let{p = \btrue} = & f(\bif{\btrue}{a}{c},\bif{\btrue}{b}{d}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & f(a,\bif{\btrue}{b}{d}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & f(a,b) \end{eqnarray*}\] and if \(p = \bfalse\), \[\begin{eqnarray*} & & f(\bif{p}{a}{c},\bif{p}{b}{d}) \\ & \let{p = \bfalse} = & f(\bif{\bfalse}{a}{c},\bif{\bfalse}{b}{d}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & f(c,\bif{\bfalse}{b}{d}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & f(c,d) \end{eqnarray*}\] as claimed.

_test_if_two_args :: (Equal a, Boolean b)
  => b -> a -> Test ((a -> a -> a) -> Bool -> a -> a -> a -> a -> Bool)
_test_if_two_args _ _ =
  testName "f(if(p,a,c),if(p,b,x)) == if(p,f(a,b),f(c,d))" $
  \f p a b c d -> eq
    (f (if p then a else c) (if p then b else d))
    (if p then f a b else f c d)

Testing

Suite:

_test_boolean ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName b, Equal b, Show b, Arbitrary b, CoArbitrary b, Boolean b
  ) => Int -> Int -> b -> a -> IO ()

_test_boolean size cases p x = do
  testLabel2 "Boolean" p x
  let args = testArgs size cases

  runTest args (_test_if_true p x)
  runTest args (_test_if_false p x)
  runTest args (_test_if_same p x)
  runTest args (_test_if_func p x)
  runTest args (_test_if_nest p x)
  runTest args (_test_if_prune_left p x)
  runTest args (_test_if_prune_right p x)
  runTest args (_test_if_commute_left p x)
  runTest args (_test_if_commute_right p x)
  runTest args (_test_if_two_args p x)

Main:

main_boolean :: IO ()
main_boolean = do
  let a = true :: Bool
  _test_boolean   20 100 a a

  _test_functions 20 100 a a a a
  _test_flip      20 100 a a a a a a a
  _test_clone     20 100 a a
  _test_compose   20 100 a a a a a a a