Distributivity laws for `GCDMonoid`

[jonathanknowles]

Hi @blamario

While reading through the documentation for GCDMonoid, I noticed this statement about distributivity laws:

If a GCDMonoid happens to also be Cancellative, it should additionally satisfy the following laws:

gcd (a <> b) (a <> c) == a <> gcd b c
gcd (a <> c) (b <> c) == gcd a b <> c

This got me thinking: must a GCD monoid be cancellative in order to satisfy the above laws?

Among the types for which instances of GCDMonoid are provided, only the following types are not Cancellative:

• IntSet
• Set a
• Product Natural

But despite non-cancellativity, these types do seem to satisfy the distributivity laws:

---

Justification

Set types

We can consider the IntSet and Set a types together, as their GCDMonoid and Semigroup instances are defined equivalently:

instance Semigroup IntSet  where (<>) = IntSet.union
instance Semigroup (Set a) where (<>) =    Set.union

instance GCDMonoid IntSet  where gcd = IntSet.intersection
instance GCDMonoid (Set a) where gcd =    Set.intersection

Of course, these types are certainly not Cancellative:

-- In order to be `Cancellative`, we must have:
(a <> b) </> b == Just a

-- If:
a = Set.fromList [0]
b = Set.fromList [0]

-- Then:
(a <> b)       ==       Set.fromList [0]
(a <> b) </> b == Just (Set.fromList [ ])
Just a         == Just (Set.fromList [0])

-- But:
Just (Set.fromList []) /= Just (Set.fromList [0])

However, we can show that they satisfy the distributivity laws.

If we substitute the above instance method definitions into the distributivity laws, we obtain:

intersection (union a b) (union a c) == union a (intersection b c)
intersection (union a c) (union b c) == union (intersection a b) c

Rewriting with traditional set notation, we obtain:

(A ∪ B) ∩ (A ∪ C) = A ∪ (B ∩ C)
(A ∪ B) ∩ (B ∪ C) = (A ∩ B) ∪ C

These are equivalent to the standard distributivity law(s) for sets, which can be proven in a number of different ways.

---

Product Natural

This type has the following Semigroup and GCDMonoid instances:

instance Semigroup (Product Natural) where (<>) = Prelude.(*)
instance GCDMonoid (Product Natural) where gcd  = Prelude.gcd

This type is also not Cancellative:

-- In order to be `Cancellative`, we must have:
(a <> b) </> b == Just a

-- If:
a = Product 1
b = Product 0

-- Then:         
(a <> b)       ==       Product 0
(a <> b) </> b == Just (Product 0)
Just a         == Just (Product 1)

-- But:
Just (Product 0) /= Just (Product 1)

But again, we can show that Product Natural satisfies the GCD distributivity laws.

If we substitute the instance method definitions above into the distributivity laws, we obtain:

Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (a * c) (b * c) == Prelude.gcd a b * c

This is equivalent to the distributivity laws for the standard gcd function on non-zero natural numbers:

gcd (ab, ac) = a * gcd (b, c)
gcd (ac, bc) = gcd (a, b) * c

But what about values of Product 0? Well it turns out that the laws still hold for zero values, since Prelude.gcd is defined such that:

Prelude.gcd 0 a == a
Prelude.gcd a 0 == a

Which means that:

-- When a = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (0 * b) (0 * c) == 0 * Prelude.gcd b c
Prelude.gcd  0       0      == 0
                     0      == 0 -- True

-- When b = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (a * 0) (a * c) == a * Prelude.gcd 0 c
Prelude.gcd      0  (a * c) == a *               c
                     a * c  == a *               c -- True

-- When c = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (a * b) (a * 0) == a * Prelude.gcd b 0
Prelude.gcd (a * b)      0  == a *             b
             a * b          == a *             b -- True

-- When a = 0, b = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (0 * 0) (0 * c) == 0 * Prelude.gcd 0 c
Prelude.gcd  0       0      == 0 *             0
             0              == 0 -- True

-- When a = 0, c = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (0 * b) (a * 0) == 0 * Prelude.gcd b 0
Prelude.gcd  0           0  == 0 *             b
             0              == 0 -- True

-- When b = 0, c = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (a * 0) (a * 0) == a * Prelude.gcd 0 0
Prelude.gcd      0       0  == a *             0
                 0          ==                 0 -- True

-- When a = 0, b = 0, c = 0:
Prelude.gcd (a * b) (a * c) == a * Prelude.gcd b c
Prelude.gcd (0 * 0) (0 * 0) == 0 * Prelude.gcd 0 0
Prelude.gcd  0       0      == 0
             0              == 0 -- True

---

Proposal

Given that all the provided instances of GCDMonoid do appear to satisfy the distributivity laws (regardless of whether or not they are Cancellative), perhaps could we simply revise the documentation for GCDMonoid to state this as a requirement, namely that all instances must satisfy the distributivity laws?

Advantages:

• Distributivity is a very useful property to have for gcd-like operations. It seems a shame that library writers can only rely on this property for the subset of GCDMonoid types that are also Cancellative.
• It would make the GCDMonoid type class more consistent with LCMMonoid, which does require that all instances satisfy the distributivity laws.
• We can remove a case of laws that are conditional on a type being instances of two classes, which seems to be a nice bonus.

I did a search over all code in GitHub that uses monoid-subclasses, but couldn't find an instance (out in the wild) that would violate these laws. I also tested all the provided instances extensively against a suite of property tests with coverage checks, and could not find a counterexample.

But perhaps I'm overlooking something? Perhaps there a good reason to keep this restriction?

If you agree this is a worthwhile simplification, let me know -- I'd be happy to make a PR that adjusts the tests and documentation. 👍🏻

Thanks for reading through, and best wishes!

Jonathan

[blamario]

I tried a quick search for the origins of that requirement and I failed. It was present in the very first Git commit of the repo. The algebraic literature search didn't uncover anything either. It was already present in the original ICFP paper, though. You've already presented a convincing-enough argument as far as Haskell goes, but I'd like to see an example of a monoid that doesn't satisfy this law, just to see what we might be giving up. I don't have the time right now, but I should be able to think this through in a few days.

[blamario]

Ok I found some time to think. One pretty clear class of counter-examples would be any non-distributive lattice, where we define <> = ∨ and gcd = ∧. The law we're discussing is exactly the definition of a distributive lattice. The Wikipedia page on lattices has some simple examples of non-distributive lattices.

A monoid-subclasses design principle is to follow the math as closely as possible, and make the classes as general as possible. Changing the laws the way you suggest would go against this principle, because one could not for example declare an instance BoundedJoinSemiLattice a => GCDMonoid a. What I'd suggest instead is to add a new class GCDMonoid a => DistributiveGCDMonoid a just for the law. It's not like the library has shied from the proliferation of law-only classes before.

[jonathanknowles]

Hi @blamario

Many thanks for coming up with this counterexample relating to non-distributive lattices.

Regarding the proposal to add a DistributiveGCDMonoid subclass: I've been giving this proposal some thought. I do have some initial ideas about this that I'd love to share with you and get your feedback on, though I'd need a bit of time to think them over more systematically.

Would it be okay if I get back to you in a few days? I'd probably need to wait until at least the weekend before I can give these ideas the attention they deserve. Hope that's okay!

All the best Jonathan

[blamario]

Of course, take your time. Ask if you have any questions, though I can't promise a prompt reply.

[jonathanknowles]

Hi Mario

After some thought, I agree with you that a DistributiveGCDMonoid subclass seems very sensible. It would potentially allow us to remove the following conditional law:

If a GCDMonoid happens to also be Cancellative, it should additionally satisfy the following laws.

Having said that, this raises a couple of interesting questions:

• What should we do with LCMMonoid? This currently requires distributivity, but under the DistributiveGCDMonoid proposal, its superclass GCDMonoid would not itself be distributive, as only DistributiveGCDMonoid would have that property.
• How can we represent non-commutative GCD monoids with distributivity?

Additionally, I noticed another inconsistency that would be really nice to solve:

• The documentation for LCMMonoid states that lcm must satisfy properties of idempotence, identity, associativity, and commutativity. However, the documentation for GCDMonoid.gcd, LeftGCDMonoid.commonPrefix, and RightGCDMonoid.commonSuffix does not mention these properties. (Though I believe they do hold for all instances provided by the library.)

With these questions in mind, what would you say to the following proposal:

Proposal

1. First create the following classes:

   -- | Class of left GCD monoids with left-distributivity.
   -- 
   -- commonPrefix (a <> b) (a <> c) == a <> commonPrefix b c
   --
   class LeftGCDMonoid m => LeftDistributiveGCDMonoid m
   
   -- | Class of right GCD monoids with right-distributivity.
   --
   -- commonSuffix (a <> c) (b <> c) == commonSuffix a b <> c
   --
   class RightGCDMonoid m => RightDistributiveGCDMonoid m

2. Then create a DistributiveGCDMonoid class, similar to your original suggestion, but with the above classes as superclasses:

   -- | Class of GCD monoids with distributivity.
   --  
   -- gcd (a <> b) (a <> c) == a <> gcd b c
   -- gcd (a <> c) (b <> c) == gcd a b <> c
   --
   class (LeftDistributiveGCDMonoid m, RightDistributiveGCDMonoid m, GCDMonoid m)
      => DistributiveGCDMonoid m

3. Then create a DistributiveLCMMonoid class:

   -- | Class of LCM monoids with distributivity.
   --
   -- (laws taken from existing distributivity laws for LCMMonoid)
   --
   class (DistributiveGCDMonoid m, LCMMonoid m) => DistributiveLCMMonoid m

4. Remove the existing statements of distributivity laws from:
   • GCDMonoid.
   • LCMMonoid.
5. Similarly to how we already document idempotence, identity, associativity, and commutativity properties in the documentation for LCMMonoid.lcm, also state these properties in the documentation for:
   • GCDMonoid.gcd
   • LeftGCDMonoid.commonPrefix
   • RightGCDMonoid.commonSuffix

Prototype

I've created a prototype of this proposal in a fork of the repository here:

• distributive-gcd-lcm-monoids

For this prototype:

• I've implemented everything in the proposal, placing new classes in the following new modules:
  • Data.Monoid.GCD.Distributive
  • Data.Monoid.LCM.Distributive
• I've added instances for each of the new classes (but only for cases where I'm confident that distributivity holds).
• I've not yet had time to make any adjustments to the monoid-subclasses test suite. However, I have tested all the instances in a prototype branch of quickcheck-monoid-subclasses.

Would be very interested to hear your thoughts on the above proposal.

If you're happy with the general direction, but want to change anything, I'd be happy to revise it.

All the best! Jonathan

[jonathanknowles]

Here's a class dependency graph for the above proposal: (source)

[blamario]

The PR looks great so far, it just needs tests. I probably wouldn't have introduced new Distributive modules for the new classes, it can be a nuisance to import multiple modules. I don't feel strongly about it though.

[jonathanknowles]

Hi @blamario

As promised, I've updated the branch and created a PR here: https://github.com/blamario/monoid-subclasses/pull/48.

Since this PR changes quite a few things, I've structured it as a series of commits. I hope that way it will be easier to review. (Each commit compiles and passes all tests.)

Regarding:

I probably wouldn't have introduced new Distributive modules for the new classes, it can be a nuisance to import multiple modules.

Thanks for mentioning this. I've changed the branch so that it adds new classes to the existing Data.Monoid.{GCD,LCM} modules instead. It required a bit of adjustment to the top-level module documentation, but I'm hoping the result is better, in that it's hopefully easier for new users to understand how the Distributive classes relate to the more general classes.

Thanks for reading through! If there's anything you'd like me to change about the PR -- let me know, would be happy to revise further. 👍🏻

Jonathan

[jonathanknowles]

Hi @blamario

Many thanks for reviewing and merging https://github.com/blamario/monoid-subclasses/pull/48!

I'm wondering, would it be convenient to make a new hackage release with the new Distributive classes?

Apologies for asking again so soon after the last time -- I know you already made a few releases recently. (If there's anything I can do to assist, am happy to help.)

All the best

Jonathan

[blamario]

No problem, just released.

[jonathanknowles]

No problem, just released.

Thanks!