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

#1

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

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 `True`s while the other one counts `False`s?

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 `Monoid`s, 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 `False`s or `True`s, respectively, thus the descriptions and names.

#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 `Monoid`s 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.