To use the example we were talking about on Slack with @sellout, the free magma can be represented as Free OPair (ordered pair) and the free commutative magma would be Free UPair (unordered pair).

OPair a is simple to define as the product of a with itself. It obviously lets you observe order: you can project out each component separately.

UPair a is harder to define, but seems reasonable that we could start with OPair a and modify it a little bit to “remove” the order.

If we have a total order on a, we might just require that the first element is less than or equal to the second element; this means that we’re never going to see UPair elements where the first is greater than the second.

That uses a subtype; the other option is to use a quotient to remove the order. To express UPair a as a quotient of OPair a, we take an equivalence relation that identifies two pairs when one is the swapped version of the other. This means that {x, y} = {y, x} (as unordered pairs).

These approaches are dual. The first approach (subtype) places constraints on the constructor of the unordered pair: you need a total order on the elements, and you need to pick which one is less than (or equal) to the other. The second approach (quotient) places constraints on the eliminator: every eliminator needs to respect the equivalence relation, so even though it gets to “see” the underlying ordered pair, the result cannot depend on what order it was actually in. Basically this says that only commutative functions can be used on UPairs, which is where the relation to commutative magmas comes in.

Mathematically, quotients are very useful and generally cleaner to work with, since you don’t need to know a total order on the elements, you don’t even have to pick representatives of the equivalence classes, and so you can preserve parametricity and abstraction and stuff. But it’s generally easier for programmers to deal with subtypes, since they can be simulated with smart constructors and, computationally speaking, you’ll be able to create a total order on your elements.

(BTW I think you can show that total orders on a are in bijection with functions UPair a -> OPair a, so these things are really equivalent ... more precisely, you can use a total order to make a map from the quotient to the subtype by always placing the smaller element first, and conversely you can ask if the function swaps its elements and build a total order out of that.)

These ideas generalize to lists, of course, but the underlying concepts are a little harder to write down formally: you need to describe monotonic lists and permutations of lists. The idea is that you can either define a multiset as a list with elements in a certain order (subtype), or as lists identified under any permutation (quotient). The first one is again much nicer to work with computationally, you just need to sort the list after each operation, and some operations can be written such that they already preserve well-sortedness.

@Nicholas Scheel I saw you post about this in the Slack. Would you mind fleshing out what this means?

Hey @Asad Saeeduddin, thanks for the ping!

To use the example we were talking about on Slack with @sellout, the free magma can be represented as

`Free OPair`

(ordered pair) and the free commutative magma would be`Free UPair`

(unordered pair).`OPair a`

is simple to define as the product of`a`

with itself. It obviously lets you observe order: you can project out each component separately.`UPair a`

is harder to define, but seems reasonable that we could start with`OPair a`

and modify it a little bit to “remove” the order.If we have a total order on

`a`

, we might just require that the first element is less than or equal to the second element; this means that we’re never going to see`UPair`

elements where the first is greater than the second.That uses a subtype; the other option is to use a quotient to remove the order. To express

`UPair a`

as a quotient of`OPair a`

, we take an equivalence relation that identifies two pairs when one is the swapped version of the other. This means that`{x, y} = {y, x}`

(as unordered pairs).These approaches are dual. The first approach (subtype) places constraints on the constructor of the unordered pair: you need a total order on the elements, and you need to pick which one is less than (or equal) to the other. The second approach (quotient) places constraints on the eliminator: every eliminator needs to respect the equivalence relation, so even though it gets to “see” the underlying ordered pair, the result cannot depend on what order it was actually in. Basically this says that only commutative functions can be used on

`UPair`

s, which is where the relation to commutative magmas comes in.Mathematically, quotients are very useful and generally cleaner to work with, since you don’t need to know a total order on the elements, you don’t even have to pick representatives of the equivalence classes, and so you can preserve parametricity and abstraction and stuff. But it’s generally easier for programmers to deal with subtypes, since they can be simulated with smart constructors and, computationally speaking, you’ll be able to create a total order on your elements.

(BTW I think you can show that total orders on

`a`

are in bijection with functions`UPair a -> OPair a`

, so these things are really equivalent ... more precisely, you can use a total order to make a map from the quotient to the subtype by always placing the smaller element first, and conversely you can ask if the function swaps its elements and build a total order out of that.)These ideas generalize to lists, of course, but the underlying concepts are a little harder to write down formally: you need to describe monotonic lists and permutations of lists. The idea is that you can either define a multiset as a list with elements in a certain order (subtype), or as lists identified under any permutation (quotient). The first one is again much nicer to work with computationally, you just need to sort the list after each operation, and some operations can be written such that they already preserve well-sortedness.

I’ll post some code later.