Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: monoids

Topic: Order Monoids

Verity Scheel (Apr 09 2020 at 03:24):

I want to talk about some monoids for ordering, in the context of Haskell/PureScript programming, just because I find it interesting :)

Verity Scheel (Apr 09 2020 at 03:31):

Haskell has a total ordering class called Ord which captures types that have a total order on them. This is useful for putting things into Sets or indexing them in Maps. Sorting, nubbing, etc.

I'll copy the PS example, bc it's easier, but Haskell is the same:

class Eq a <= Ord a where
  compare :: a -> a -> Ordering

Where (Ordering)[https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Data.Ordering#t:Ordering] is a three-element monoid:

data Ordering = LT | GT | EQ

instance semigroupOrdering :: Semigroup Ordering where
  append LT _ = LT
  append GT _ = GT
  append EQ y = y

instance monoidOrdering :: Monoid Ordering where
  mempty = EQ

invert :: Ordering -> Ordering
invert GT = LT
invert EQ = EQ
invert LT = GT

It has two left-absorbing elements and the identity. It turns out that it captures lexical orders on products very well: if we have a product (a, b) then we have compare (a, b) (c, d) = compare a c <> compare b d (where we write <> for the semigroup operation).

Verity Scheel (Apr 09 2020 at 03:34):

It also has one non-trivial involution which can be used to state one of the laws: compare a b = invert (compare b a) (actually, I'm not sure what law that actually is … antisymmetry?)

Verity Scheel (Apr 09 2020 at 03:38):

It also has a nice homomorphism areEq to the Boolean monoid under conjunction, which we call Conj Boolean in PS, that sends the non-empty elements to false. This can be used to state the expected behavior WRT to the parent class Eq: areEq (compare a b) == (a == b).

Verity Scheel (Apr 09 2020 at 03:40):

Total orderings are nice for sorting and other computational things, but partial orderings are more common for capturing the semantics of some datatypes. Can we also describe them with a monoid?

Dan Doel (Apr 09 2020 at 03:44):

I think for products, you might have a lattice.

Verity Scheel (Apr 09 2020 at 03:45):

The answer is yes, of course! I just had to make it myself:

data POrdering = PLT | PEQ | PGT | UNC

instance semigroupPOrdering :: Semigroup POrdering where
  append UNC _ = UNC
  append _ UNC = UNC
  append PEQ a = a
  append a PEQ = a
  append PLT PLT = PLT
  append PLT PGT = UNC
  append PGT PLT = UNC
  append PGT PGT = PGT
instance monoidPOrdering :: Monoid POrdering where
  mempty = PEQ

inverse :: POrdering -> POrdering
inverse PLT = PGT
inverse PGT = PLT
inverse PEQ = PEQ
inverse UNC = UNC

This time we have three idempotent elements and the identity: one absorbing element, and two that annihilate each other (i.e. PGT <> PLT == UNC == PLT <> PGT).

We still have the nice homomorphism and involution as mentioned above. But notice that it's commutative now!

Verity Scheel (Apr 09 2020 at 03:46):

Now our interpretation for products is that pcompare (a, b) (c, d) = pcompare a c <> pcompare b d and the more familiar semantics is that (a, b) <= (c, d) when a <= b and c <= d

Dan Doel (Apr 09 2020 at 03:46):

Yeah, that lattice.

Dan Doel (Apr 09 2020 at 03:47):

PEQ is the bottom, UNC is the top, and you take joins.

Dan Doel (Apr 09 2020 at 03:47):

Or flip it upside down.

Dan Doel (Apr 09 2020 at 03:48):

Seems suggestive that you're classifying two values of a partial order by mapping them to a lattice (which is also a partial order).

Verity Scheel (Apr 09 2020 at 03:50):

I hadn't actually thought about it that way, but yes! One of the simplest lattices

Verity Scheel (Apr 09 2020 at 03:52):

We can generate an ordering function from a partial order >= operator:

fromGERelation :: forall t.
  (t -> t -> Boolean) ->
  (t -> t -> POrdering)
fromGERelation f a b =
  case f a b, f b a of
    true, true -> PEQ
    true, false -> PGT
    false, true -> PLT
    false, false -> UNC

Dan Doel (Apr 09 2020 at 03:52):

Or, I guess the process I meant is more complicated. Classifying a compound partial order by mapping to a 'simpler' partial order and combining there.

Verity Scheel (Apr 09 2020 at 03:55):

You can factor products out. Is that a good phrasing? I'm not quite sure ...

Verity Scheel (Apr 09 2020 at 03:57):

One reason why we use (p)compare to define an order, instead of the mathematical convention of <=, is computational efficiency: we might as well give all the information we have at once, instead of computing both <= and >=, which would be wasteful.

Verity Scheel (Apr 09 2020 at 04:08):

Is there a name for the standard product partial order? I guess it would be the categorical product … but I find it interesting how different the lexical order and the partial product order are. They essentially never agree, even though they are both the natural choices for ordering products in closely related ways (only one extra law for total orders).

Dan Doel (Apr 09 2020 at 04:14):

It's the categorical product, which is also the product of the partial orders considered to be categories, I believe. I'm not sure if there's a nice characterization of the lexicographic order.

Verity Scheel (Apr 09 2020 at 04:19):

The lexicographic order probably cannot be specified using a universal property, because it is not invariant under isomorphism … (a, b) <= (c, d) isn't the same as (b, a) <= (d, c). Does that seem right? I'm too tired rn to actually check the categorical details lol

Dan Doel (Apr 09 2020 at 04:20):

Well, it can't be a construction that's commutative.

Dan Doel (Apr 09 2020 at 04:30):

nlab doesn't have anything particularly nice categorically to say about it.

Verity Scheel (Apr 09 2020 at 04:35):

One more note before I go to bed: my particular application of partial orders in the above project was resolving ambiguity during parsing. For each parsing rule I knew was ambiguous, I would look at the AST and assign disambiguation precedences, and then I would look for a parse that was maximally preferred over all others. If, at the end of this discarding, there was still not a unique parse, then I would fail parsing, but so far I haven't seen an instance of that happen: The assumption is that parse ambiguity is roughly compositional, so if there are two ambiguous rules that can both individually trigger on the same string, there should be a case where both of their preferred parsings were found.

Lê Thành Dũng (Tito) Nguyễn (Apr 09 2020 at 12:27):

BTW, the three-element monoid LT | GT | EQ is known in the literature as the "flip-flop monoid" cf. https://en.wikipedia.org/wiki/Semigroup_with_three_elements