Add redundant fields to algebraic structures to make diamonds commute

[laMudri]

This pull request is an experiment in doing what I suggested in #898. The guiding principle is that when giving an instance of a subclass, all of the fields of its superclasses should be accessible. This is currently violated in, for example, CommutativeMonoid. The supporting definition IsCommutativeMonoid is currently the following.

record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup public

  identityʳ : RightIdentity ε ∙
  identityʳ = Consequences.comm+idˡ⇒idʳ setoid comm identityˡ

  identity : Identity ε ∙
  identity = (identityˡ , identityʳ)

  isMonoid : IsMonoid ∙ ε
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = identity
    }

  isCommutativeSemigroup : IsCommutativeSemigroup ∙
  isCommutativeSemigroup = record
    { isSemigroup = isSemigroup
    ; comm        = comm
    }

It violates the stated principle because it is impossible to give a specific proof of identityʳ. Instead, we must accept the proof of identityʳ that goes via identityˡ and comm.

Problems with the current definition come about under these circumstances:

1. Such a definition appears in the middle layer of an inheritance diamond.
2. We care about the diamond commuting (up to definitional equality).

The outcome is that it gets difficult to parametrise over algebraic structures, as one would like to do for modules over a ring, for example (#897).

The particular diamond in the case of CommutativeMonoid is

      AbelianGroup
     /            \
Group              CommutativeMonoid
     \            /
         Monoid

IsAbelianGroup happens to be defined with an IsGroup field, meaning that it does have an identityʳ field. This, therefore, is thrown away by the embedding into CommutativeMonoid, and gets reconstructed in the embedding of CommutativeMonoid into Monoid. Thus, this diamond does not commute definitionally.

---

In this pull request, IsCommutativeMonoid has the following definition.

record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMonoid : IsMonoid ∙ ε
    comm     : Commutative ∙

  open IsMonoid isMonoid public

  isCommutativeSemigroup : IsCommutativeSemigroup ∙
  isCommutativeSemigroup = record
    { isSemigroup = isSemigroup
    ; comm        = comm
    }

Additionally, for convenience and some level of compatibility, there are new definitions IsCommutativeMonoidˡ and IsCommutativeMonoidʳ, with the former defined as follows. Having both of these definitions means that we're no longer biased towards the identityˡ law – we could give only the identityʳ law (via IsCommutativeMonoidʳ) instead.

record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup

  private

    identityʳ : RightIdentity ε ∙
    identityʳ = Consequences.comm+idˡ⇒idʳ setoid comm identityˡ

    identity : Identity ε ∙
    identity = (identityˡ , identityʳ)

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = record
      { isSemigroup = isSemigroup
      ; identity    = identity
      }
    ; comm = comm
    }

  open IsCommutativeMonoid isCommutativeMonoid public
    hiding (identityˡ)

The intended method of using this structure looks something like the following.

commutativeMonoid : CommutativeMonoid c ℓ
commutativeMonoid = record
  { Carrier = Something
  ; _≈_ = _≈_
  ; _∙_ = _∙_
  ; ε = ε
  ; isCommutativeMonoid = IsCommutativeMonoidˡ.isCommutativeMonoid record
    { isSemigroup = ...
    ; identityˡ = ...
    ; comm = ...
    }
  }

These structures do not get their own bundles, as they shouldn't be used for any purpose other than the last example.

---

This branch will currently not build, as I haven't inserted the coercions throughout the library. A quick grep suggests that there are 20 CommutativeMonoid instances to fix, plus (probably fewer) instances of CommutativeSemiring and Ring. I want to get most of the design done before making lots of changes throughout the library.

[ajrouvoet]

I think this is the right hierarchy.

That being said, I have found that it does not necessarily play nice with instance search if that would ever become default for the std lib.

The issue there is (I think) that it is not possible to mark the isCommutativeSemigroup instance with overlap, as one would (perhaps) mark a field. For a specific type I might want to give an instance of IsCommutativeSemigroup separately because it is available under few assumptions than the Monoid instance (e.g., for products). There is always {-# OPTIONS --overlapping-instances #-}, but in practice you want to avoid this due to performance issues.

[ajrouvoet]

FWIW, that is probably not a problem specific to this PR, but might equally apply to the current hierarchy. But if we're going to make breaking changes, it might be worth considering instance search, which has become more reliable now that it doesn't do backtracking by default.

[laMudri]

This is something I don't know much about and haven't thought about at all. Are there the same problems with instance search for CommutativeRing, which already has redundant fields (and where there is the diamond CommutativeRing ≤ Ring/CommutativeSemiring ≤ Semiring)?

[ajrouvoet]

I haven't tried changing the definitions to support instance search, but I would be extremely surprised if the current definitions work well out of the box. A similar diamond in a different setting which does use instance search gave me quite a few headaches.

[laMudri]

Do you have a (non-)working example? I feel that I half-understand what the problems might be, but can't put them together to see what goes wrong. How would any diamonds be handled by instance search, for example?

[ajrouvoet]

I started trying it out with the stdlib's definitions but ran into too many name clashes to quickly produce an example.

What I'm trying to say is: if the std library intends to start making use of instance search more, we should expect breaking changes to the algebra hierarchy. Since this PR also proposes breaking changes (for the better), we should consider combining both and not bother people twice :)

If instance search for the std lib is not on the agenda, then my concerns are a non-issue.

[MatthewDaggitt]

Thanks @laMudri, this looks pretty good. I have a couple of comments though:

I'd ideally like to keep the left and right biased versions very minimal to discourage their use as much as possible, i.e. just

record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙

we could then have a function commutativeMonoidˡ : IsCommutativeMonoidˡ ∙ ε -> IsCommutativeMonoid ∙ ε that handles the translation. In order to fix people's code all they would have to do is prepend that function to their existing record definitions. I'm open to snappier names for the functions.

I'm also thinking that maybe we should have them in a different module, maybe Algebra.Structures.Biased? The main algebra hierarchy is complicated enough as it is!

Finally Semilattice vs Lattice would be another one that'd be great to fix. It's been my particular bug bear for a while.

What I'm trying to say is: if the std library intends to start making use of instance search more, we should expect breaking changes to the algebra hierarchy. Since this PR also proposes breaking changes (for the better), we should consider combining both and not bother people twice :) If instance search for the std lib is not on the agenda, then my concerns are a non-issue.

It's definitely on a lot of people's agenda: about every 6 months or so we have someone keen to improve the standard library's support for instance search. The problem is that no-one as of yet has come up with concrete proposals about what to include and how to organise it. We're definitely open to any suggestions for the design though 👍

[ajrouvoet]

Would we need the left/right biased structures at all if Agda had default field implementations like Haskell?

[ajrouvoet]

It's definitely on a lot of people's agenda: about every 6 months or so we have someone keen to improve the standard library's support for instance search. The problem is that no-one as of yet has come up with concrete proposals about what to include and how to organise it. We're definitely open to any suggestions for the design though

I'm developing a hierarchy of partial algebras (e.g., IsPartialCommutativeMonoid <: IsPartialMonoid <: IsPartialSemigroup) where the binary operation is represented by a partial, non-functional ternary relation in Agda. The setup is pretty close to what is in this PR, but uses instance search. I'll be releasing it soonish as an artifact for a CPP '20 paper. It could probably serve as a first design draft for the use of instances in the standard library.

[laMudri]

Would we need the left/right biased structures at all if Agda had default field implementations like Haskell?

I see IsCommutativeMonoidˡ and the like as doing default implementations manually. That said, even then it would be hard to reach into the isMonoid field and give a default implementation of its identityʳ field, purely because we happen to have given isMonoid's identityˡ field and the comm field. But if we could do that, we'd get rid of these helper modules, I guess.

I'd ideally like to keep the left and right biased versions very minimal to discourage their use as much as possible

Yeah, I could get behind this.

we could then have a function commutativeMonoidˡ : IsCommutativeMonoidˡ ∙ ε -> IsCommutativeMonoid ∙ ε that handles the translation.

I quite like the trick of this function being a member of IsCommutativeMonoidˡ, which could have a simpler name than IsCommutativeMonoidˡ.isCommutativeMonoid (something like IsCommutativeMonoidˡ.mk). I think it signals the intention fairly well from a single place. It also allows having far less messy type signatures, because we don't have to reintroduce all of the operators.

I'm also thinking that maybe we should have them in a different module, maybe Algebra.Structures.Biased? The main algebra hierarchy is complicated enough as it is!

Also agreed. It's a good property that these definitions play no role in the algebra hierarchy, and we can signal that by putting them somewhere else, where they're not depended on. Maybe we could find a nicer name. Somehow these definitions should only be used transiently, but they shouldn't be totally discouraged.

Finally Semilattice vs Lattice would be another one that'd be great to fix. It's been my particular bug bear for a while.

Could this be done in a separate PR? IIRC, this is an orthogonal issue.

[laMudri]

Ah, I guess you have this in mind:

-- Note that `IsLattice` is not defined in terms of `IsSemilattice`
-- because the idempotence laws of ∨ and ∧ can be derived from the
-- absorption laws, which makes the corresponding "idem" fields
-- redundant.  The derived idempotence laws are stated and proved in
-- `Algebra.Properties.Lattice` along with the fact that every lattice
-- consists of two semilattices.

Then yes, this PR is a decent place to go against this comment.

But then we have the concerns from #676. Did we come to any kind of consensus? It seems clear than both the algebraic and the order theoretic views of lattices are valid, in a way that IsCommutativeMonoidˡ is not valid. But should the algebraic BoundedSemilattice and IdempotentCommutativeMonoid be aliased or not? And do we rename the operator from _∙_ to one (or both) of _∧_ and _∨_?

[JacquesCarette]

Sorry that it took a while for me to comment on this - too many deadlines, and as this is an issue I care about a lot, it needs a decent block of time to respond properly.

The foundational inspiration of this PR, namely

The guiding principle is that when giving an instance of a subclass, all of the fields of its superclasses should be accessible.

and

It violates the stated principle because it is impossible to give a specific proof of identityʳ. Instead, we must accept the proof of identityʳ that goes via identityˡ and comm.

are spot on. However, you happened to notice a particular diamond that was a problem, whereas in a fuller Algebra hierarchy, there are hundreds of them. In my old prototype , there is an Algebra library with 512 diamonds in it. Closer to Agda proper, we have an eslip prototype that does meta-programming to generate the kinds of things you are currently doing by hand (i.e. it generates Agda that typechecks). Its library (I don't have the link handy) has about 300 algebraic structures in it. The theory behind that is described in a submitted journal paper.

Of course, none of that is ready for prime time, yet. Though I think useful background material.

On the details of what you're doing here: first, you should note that this left/right diamond you've encountered really belongs as LeftUnitalMagma and RightUnitalMagma rather than at the Monoid level. The Monoid incarnation is the colimit of the above diamond (over UnitalMagma) with the 'extension' that adds associative (i.e. the extension of Magma to Semigroup) and the 'extension' that add commutative (i.e. from Magma to CommutativeMagma). People are much less interested in non-associative algebras, but they do crop up enough that it's worth knowing that this is an issue.

Roughly speaking, any rigid record 'hierarchy' is going to fail -- there are simply way too many diamonds to hope to "get it right".

Having said that, because there is no alternative suggestion at hand, it is worthwhile evaluating what you propose here "on its own merits", to see if it is a step forward. Yes, I do think this is an improvement. [And that the improvements that one can make to Lattice ought to be done in a separate PR]. But I would not encourage wholesale changes in this direction, as it is long-term doomed. The 'structure' inside algebra is much more complex than just simple inclusions. One can find 'n-dimensional cubes' in there (you showed n=2), with n=5 or 6 fairly easily. Luckily, these are all structural, so there is meta-theory that does say you can capture them.

[JacquesCarette]

While I was writing the above, once more comment came in.

The issue around BoundedSemilattice, IdempotentCommutativeMonoid, etc, is much more complex. First, as you note, there is a real need for renaming. A Lattice ought to have _∧_ and _∨_ in it for usability. So using aliasing seems like a really bad idea.

Furthermore, the additional comments (about redundancy of fields) shows that, in even for things that end up being equivalent, what fields have to be primitive, and which can be derived, is very (very!) tricky. The issues, unlike above, are no longer structural: the 'theory presentation morphisms' involved are not embeddings, they are full views. When you have views in both directions, this is a situation where Realms are a useful idea (if it was actually implemented...). Yes, in HoTT, this is regarded as "free", if you're a theoretician who doesn't care about computational matters (HoTT people will, when pressed, admit that 'transport' can indeed involved arbitrary computations). I am adverse to hiding arbitrary computations, so I prefer to make those kinds of 'coercions' explicit.

That's all a long winded way to say that the isomorphism between BoundedSemiLattice and IdempotentCommutativeMonoid should be explicit, because it involves a computation. It is not a structural isomorphism, as it can indeed involve not just axioms (i.e. fields) but also derived theorems, in its definition. In some ways, the better view of that isomorphism is probably 2-categorical, where the resulting 2-category is not strict.

[laMudri]

To pick off stuff I can respond to quickly:

One can find 'n-dimensional cubes' in there (you showed n=2), with n=5 or 6 fairly easily.

Do you have a simple example? This seems believable, but an example would serve as good motivation and make sure everyone is on the same page. I can imagine things getting difficult like this if you start mixing algebra and order (so that all operators are monotonic, have some properties, and you can also separately take meets/joins).

there is a real need for renaming. [...] So using aliasing seems like a really bad idea.

There is a middle ground. In particular, it's possible to have BoundedSemilattice = IdempotentCommutativeMonoid, but have module BoundedSemilattice be distinct from module IdempotentCommutativeMonoid. Here is a quick mock-up:

record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier                       : Set c
    _≈_                           : Rel Carrier ℓ
    _∙_                           : Op₂ Carrier
    ε                             : Carrier
    isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∙_ ε

  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public

  commutativeMonoid : CommutativeMonoid _ _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (rawMagma; magma; semigroup; rawMonoid; monoid)


BoundedMeetSemilattice = IdempotentCommutativeMonoid

module BoundedMeetSemilattice {c ℓ} (idemCommMonoid : IdempotentCommutativeMonoid c ℓ) where
  open IdempotentCommutativeMonoid idemCommMonoid public
    renaming (ε to ⊤; _∙_ to _∧_; et cetera...)

Alternatively, they could share content in Algebra.Structures but have separate records in Algebra.Bundles. Anyway, there are a lot of choices, and as far as I remember, the algebraic presentation of BoundedSemilattice is close enough to IdempotentCommutativeMonoid for some sharing to make sense.

When they are incorporated into (Bounded)Lattice, we can do the same renaming as we do for semirings made of two monoids, so this should not be an issue.

[JacquesCarette]

In some ways, one can claim that right above Magma there should be a weird 18-dimensional cube -- see all the properties that can be defined on a single binary operation. (There are more than 18 there, some are vertices of that cube). Of course, via proof, one can show that many of those dimensions collapse. If instead you start from a signature with 2 binary operations and 2 points, there are a huge number of axioms that you can add independently without having everything collapse.

More convincing is the full 4D cube sitting in modal logics around S3 -- see about 40% of the way down on Halleck's list of modal logics page. Note that that link is to a mirror, as the 'main' page seems down right now.

It gets weird when you mix in order. There are valid structures that are monotonic for some operations but not all - sorry, I don't remember which ones.

So the mockup you give gives a module for BoundedMeetSemilattice, but what I want is a record with those fields. I did not think that was possible with renaming as above. I would love to be wrong on this!!

[laMudri]

To bring this back to the issue at hand, it seems that both of the prototype libraries don't try to address redundancy of axioms in the presence of more structure, which is what is causing the complexity here. Yes, the inheritance hierarchy could be better with some more technology, but this only helps when giving instances and adding to the hierarchy. When using structures, we can just open everything, and the difference between fields and fields of fields, and even defined records made up only of fields, goes away. What this pull request does is to ensure that fields don't turn into complex auxiliary definitions, which does matter in usage sometimes.

I think the best course of action at the moment is to define the scope of this PR, and then press on. From a quick look through, it seems that we have the following modules that may need changing if we decide that the changes here are good:

• Algebra.Morphism
• Algebra.Morphism.Structures
• Algebra.Structures
• Function.Structures
• Relation.Binary.Indexed.Heterogeneous.Structures
• Relation.Binary.Indexed.Homogeneous.Structures
• Relation.Binary.Lattice
• Relation.Binary.Morphism.Structures
• Relation.Binary.Structures

This is just all of the Structures modules, plus other things I could find. So far, I have tackled part of Algebra.Structures. The other half, i.e the lattice-like structures, need more serious fixes, so I'm going to leave that for another PR. As for the others, here's what they seem to have:

• Algebra.Morphism – in here, IsGroupMorphism contains a surprising definition of ⁻¹-homo. This is not used to fill any fields from earlier in the hierarchy, so may be fine.
• Algebra.Morphism.Structures – this seems to be in a state of development, with nothing problematic yet.
• Function.Structures – this is full of diamonds, the likes of which Jacques et al's work would improve. However, no shortcuts are taken, so these are fine.
• Relation.Binary.Indexed.*.Structures – these modules do not contain much yet, so there is not much to go wrong. They mirror Relation.Binary.Structures to an extent, so if the latter is dealt with the former will be.
• Relation.Binary.Lattice – IsDistributiveLattice contains a field ∧-distribˡ-∨. By standard lattice theory, we should have a whole bunch more distributivity laws derived from this, but they do not appear. Maybe we should define IsDistributive{Join,Meet}Semilattice as superclasses, and then give lots of biased constructors. Additionally, IsBooleanAlgebra forces the exponential to be defined in terms of ¬_ and _∨_, which may not always be what we want.
• Relation.Binary.Morphism.Structures – this module is somewhat similar to Function.Structures, and is fine.
• Relation.Binary.Structures – the only dubious part is IsStrictTotalOrder, which totally ignores the hierarchy and does its own thing with the compare field. This is perhaps justified in being a totally different view of relations than what the rest of the module has, like with the case of lattices in order theory vs in algebra. This is also affected by the lingering issue of doing what I did to Dec to the Tri type.

I think each of the 2 or 3 modules that need work, plus the things about algebraic lattices, would fit into their own pull requests. As such, I'll start work on making the library typecheck after the changes I've made so far, and see how it goes. I still consider this pull request an experiment, so I'd like to see this sample through.

[JacquesCarette]

I think your assessment makes a lot of sense, as does your plan.

[laMudri]

That's the library checking again. There aren't really too many changes needed, so that's a good thing. I've tended to use the biased structures only when the properties they derive aren't already proven. In fact, I've only used biased structures in Data.List.Relation.Binary.BagAndSetEquality and Function.Related.TypeIsomorphisms. In the cases where I didn't use biased structures, the transformation either made the instances shorter or involved exporting more (potentially useful) structures, like an IsMonoid to go with each IsCommutativeMonoid.

The most work per instance seemed to be caused by IsCommutativeSemiring. I'm considering making the canonical definition more like the existing one. At the moment, the definition is semiring + * is commutative, whereas it used to be two commutative monoids + distrib & zero. My reason for the former was to make IsCommutativeSemiring more like IsCommutativeRing, and also increase reuse slightly. But maybe slightly better backwards compatibility is worth more than that. If I do make this change, I would also introduce IsCommutativeSemiringFromSemiring, which turns semiring + commutative * into the canonical IsCommutativeSemiring.

[JacquesCarette]

The changes are quite modest and straightforward - I agree that's a good sign. Many are indeed improvements.

BTW, it seems odd to me that semiring is commutative by default.

[laMudri]

BTW, it seems odd to me that semiring is commutative by default.

There must be some misunderstanding here. stdlib has both Semiring and CommutativeSemiring, differing on whether _*_ is commutative. This is entirely standard.

[JacquesCarette]

I think it was my misunderstanding of your statement

At the moment, the definition is semiring + * is commutative, whereas it used to be two commutative monoids + distrib & zero.

I guess you meant CommutativeSemiring ?

[laMudri]

What I meant to say here is that IsCommutativeSemiring is defined via IsSemiring and Commutative _*_. It used to be defined via IsCommutativeMonoid _+_ 0#, IsCommutativeMonoid _*_ 1#, and fields for distributivity and zero (annihilation). That part wasn't the clearest!

[MatthewDaggitt]

Looks good. A couple more comments.

[MatthewDaggitt]

Oh and we need a changelog entry explaining the changes.

[laMudri]

Thanks for all the comments today. I'll probably go through them seriously tomorrow, as well as having a look at some of the other areas I identified in this thread a few comments back. It just works out that this timing has worked out well for me. 🙂

[MatthewDaggitt]

Okay, looks like this has settled down. I'll merge it in tomorrow unless anyone has any more comments?