What's up with Bool/even and Bool/odd?

#1

Bool/even:

Returns True if there are an even number of False elements in the list and
returns False otherwise

Bool/odd:

Returns True if there are an odd number of True elements in the list and
returns False otherwise

What was the motivation for adding these functions? Why does one function count Trues while the other one counts Falses?

The commit introducing them doesn’t provide any context.

#2

@sjakobi: All of Dhall’s operators (except for . and the proposed ≡ operator for equivalence) form Monoids, meaning that they are associative and have some identity element. For each such operator I tried to add the corresponding mconcat to the Prelude where possible. For example, the mconcat for the + operator is Natural/sum and the mconcat for # is List/concat.

I added Bool/{even,odd} since they provide the mconcat for == and !=, respectively. They exist purely for symmetry and are not motivated by a practical use case. When naming them I tried to come up with an intuitive description of what they did. It turns out that the easiest way to reason about their behavior is to think of them in terms of counting either Falses or Trues, respectively, thus the descriptions and names.

1 Like
#3

Thanks for the explanation, @Gabriel439!

I think it would be good to document that Bool/even and Bool/odd mostly serve to demonstrate the monoidal properties of == and !=.

I also wonder whether we could use the proposed assert to prove that Monoids in the prelude actually obey the stated law:

t  : Type
f  : ./Monoid t
xs : List (List t)

f (./List/concat t xs) = f (./map (List t) t f xs)

But I suspect that we’d need additional simplifications.