§ We can't define choice for finite sets in Haskell!
If all you have is a decidable equality relation on the elements, then
there seems to be no function which can implement choice. That is, you can’t
write a function choose :: Set a -> Maybe (a, Set a)
Concretely, suppose we represent sets as lists of nonrepeated elements. Then,
we can write an operation choose :: Set a -> Maybe (a, Set a), which just
returns a pair of the head and the tail if the list is nonempty, and returns
Nothing if it is empty.
However, this operation does not respect equality on sets. Note that any
permutation of a list representing a given set also represents that same set,
but the choose operation returns different answers for different permutations.
As a result, this operation is not a function, since it does not behave
extensionally on finite sets!
I feel there should be an argument involving parametricity which makes this
work for arbitrary datatype representations, since all we rely on is the fact
that equality can’t distinguish permutations. But I haven’t found it yet.