Sorted Lists and Free Idempotent Commutative Monoids

Abstract: Free monoids are very well-understood and widely used, both on paper and in code. However, their commutative cousins are slightly trickier to pin down a neat data type for. There is a well-established mathematical story involving finite multisets, but they are notoriously tricky to implement sensibly in code. Instead, I want to focus on a datatype for sorted lists which turns out to be nearly the same thing if you squint the right way. I'll first demonstrate how we can construct and work with these things, and then the squinting shall begin! We can easily show it to be a commutative monoid, but thinking of it as the free one will require adopting the correct perspective. Specifically, we'll need to work in the land of total orders rather than sets. I'm actually interested in finite subsets rather than finite multisets, and that pleasingly only requires adding idempotency to the monoid multiplication, and strictness to the total order. Although, this actually leads to some interesting wrinkles when we try to prove freeness.