[ re #1752 ] add properties of ordered structures for Nat.

[sstucki]

Follow-up to #1752, implementing the new ordered structures for Data.Nat. The PR currently replaces the old (unordered) proofs by ordered ones and then re-exports derived versions of the old ones. The re-exports are named so as to retain backwards compatibility. If desired, I can refactor the PR to keep the old proofs.

[sstucki]

Shout-out to @Taneb who originally suggested implementing this PR.

[MatthewDaggitt]

That's okay, no worries, I can do the refactoring myself at AIM tomorrow.

[MatthewDaggitt]

@sstucki just doing this now. The first thing I notice is that the fields of IsSemiring and IsPosemiring are not symmetric? Is there a reason why not?

[sstucki]

@sstucki just doing this now. The first thing I notice is that the fields of IsSemiring and IsPosemiring are not symmetric? Is there a reason why not?

Sorry @MatthewDaggitt, I don't understand what you mean by "symmetric". Can you give an example?

[MatthewDaggitt]

Definition of IsSemiring:

record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1#
    zero : Zero 0# *

Definition of IsPosemiring:

record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    +-isCommutativePomonoid : IsCommutativePomonoid + 0#
    *-mono                  : Monotonic₂ _≤_ _≤_ _≤_ *
    *-assoc                 : Associative *
    *-identity              : Identity 1# *
    distrib                 : * DistributesOver +
    zero                    : Zero 0# *

I'd expect it to be:

record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPosemiringWithoutAnnihilatingZero : IsPosemiringWithoutAnnihilatingZero _≤_ + * 0# 1#
    zero : Zero 0# *

[sstucki]

I'd expect it to be:

record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPosemiringWithoutAnnihilatingZero : IsPosemiringWithoutAnnihilatingZero _≤_ + * 0# 1#
    zero : Zero 0# *

Oh, I see. Indeed, I skipped a few intermediate structures. There's no good reason for that other than, when I first mechanized the ordered structures, the algebraic hierarchy was a lot simpler. Also, to be honest, I have no idea where you'd ever use a PosemiringWithoutAnnihilatingZero, and I figured people could create their own PRs if they ever did. In other words, I was lazy.

[MatthewDaggitt]

Also, to be honest, I have no idea where you'd ever use a PosemiringWithoutAnnihilatingZero, and I figured people could create their own PRs if they ever did

So if it's been added, it's been used. The problem is that if it was added then the record definition of IsPosemiring couldn't be updated in a backwards compatible manner. This problem is what I was trying to get across in my review in the previous PR. The algebra hierarchy is complicated and messy, and using the orders as the base records means that we end up having to duplicate that messiness and keep it in sync....

[sstucki]

The problem is that if it was added then the record definition of IsPosemiring couldn't be updated in a backwards compatible manner.

I don't understand what you mean by that.

This problem is what I was trying to get across in my review in the previous PR. The algebra hierarchy is complicated and messy, and using the orders as the base records means that we end up having to duplicate that messiness and keep it in sync....

But that would still be the case if the algebraic structures would be at the base, no? You'd still need two new definition for each of the definitions in the hierarchy. Even if those new definitions would just be adding the pre/partial order components. Or am I missing something?

[sstucki]

BTW, if you want me to "fill in" the missing structures in the Algebra.Ordered hierarchy for the sake of symmetry, I don't mind doing that. I'm less eager to add new structures that are not directly involved in the current ordered hierarchy (e.g. SelectivePomagma). I guess those would be easy to add in the future if someone needs them without having to touch what is there now. Maybe that's what you meant by records that could "be updated in a backwards compatible manner"?

[MatthewDaggitt]

Apologies for the delay in replying.

The problem is that if it was added then the record definition of IsPosemiring couldn't be updated in a backwards compatible manner.

I don't understand what you mean by that.

You couldn't change the definition of IsPosemiring from

record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    +-isCommutativePomonoid : IsCommutativePomonoid + 0#
    *-mono                  : Monotonic₂ _≤_ _≤_ _≤_ *
    *-assoc                 : Associative *
    *-identity              : Identity 1# *
    distrib                 : * DistributesOver +
    zero                    : Zero 0# *

to

record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPosemiringWithoutAnnihilatingZero : IsPosemiringWithoutAnnihilatingZero _≤_ + * 0# 1#
    zero : Zero 0# *

without breaking people's code. If you didn't make the change, then the two hierarchies wouldn't be symmetric which would be very surprising to users.

This problem is what I was trying to get across in my review in the previous PR. The algebra hierarchy is complicated and messy, and using the orders as the base records means that we end up having to duplicate that messiness and keep it in sync....

But that would still be the case if the algebraic structures would be at the base, no? You'd still need two new definition for each of the definitions in the hierarchy. Even if those new definitions would just be adding the pre/partial order components. Or am I missing something?

No it would not be the case. Let's draw a picture of the current complicated and messy hierarchy in Algebra.Structures

The approach to the Algebra.Ordered hierarchy that we've taken so far is to duplicate that structure as follows (purple for Pro structures, blue for Po structures:

So if the base Algebra.Structures hierarchy changes, (as it regularly does unfortunately), then with the current setup we have to duplicate the work 3 times and make 3 sets of backwards incompatible changes.

In contrast what I would like is the following organisation:

Here, if the base Algebra.Structures hierarchy changes, then nothing needs to be changed. We do the hard bit once in Algebra.Structures, and then simply piggy back of that work in Algebra.Ordered.Structures

BTW, if you want me to "fill in" the missing structures in the Algebra.Ordered hierarchy for the sake of symmetry, I don't mind doing that. I'm less eager to add new structures that are not directly involved in the current ordered hierarchy (e.g. SelectivePomagma)

That's exactly what I'm trying to avoid you having to do 😄. With the approach directly above, it doesn't matter that you've left them out. They can easily be filled in later, by simply extending the diagram upwards.

I do understand that having to provide a congruence proof directly when it should be inferrable is a little bit irritating, but it's exactly that, irritating. Unlike duplicating proofs within the same record structure, It doesn't affect the theory, and I honestly don't think that it's worth the pain of all the bugs and breaking changes I'm almost postive we're going to continuously get if we stick with the current structure.

[sstucki]

Thanks for the nice diagrams @MatthewDaggitt, they are very helpful. But I don't entirely buy it. You say

Here, if the base Algebra.Structures hierarchy changes, then nothing needs to be changed.

That can't be right. First, the vertical branches in your second picture don't magically appear, someone still has to add them. Also, code that depends on the base hierarchy still breaks if that changes. And finally, the records wouldn't just contain the extra fields representanted by the vertical branches, they would also contain convenience definitions and re-exports of the related (ordered) algebraic structures. E.g. a promonoid would contain a field prosemigroup and export those members of the prosemigroup that are not members of the underlying semigroup (e.g. promagma), and so on. So the real picture would be a sort of overlay of your two pictures, and maintaining it would still be tricky.

But I get your point, fewer things would break if one decided to establish the "symmetry" between the different "levels" of the pictures in a lazy fashion. I guess. Then again, you just argued against having an asymmetric set of hierarchies:

If you didn't make the change, then the two hierarchies wouldn't be symmetric which would be very surprising to users.

So then I guess one would really have just as much breaking code and maintenance anyway?

[MatthewDaggitt]

Here, if the base Algebra.Structures hierarchy changes, then nothing needs to be changed.

That can't be right. First, the vertical branches in your second picture don't magically appear, someone still has to add them.

Sorry, yes you're right that was imprecise phrasing on my behalf. The point is that missing vertical branches can be added in a backwards compatible manner, and therefore don't need to be all added at the same time. In contrast, if you miss out one of the nodes in the second diagram then it's impossible to add it in in a backwards compatible manner.

Also, code that depends on the base hierarchy still breaks if that changes.

That's the thing though, yes the code in the library breaks and yes the user's original algebra code breaks, but their code building the ordered structures doesn't right?

And finally, the records wouldn't just contain the extra fields representanted by the vertical branches, they would also contain convenience definitions and re-exports of the related (ordered) algebraic structures. E.g. a promonoid would contain a field prosemigroup and export those members of the prosemigroup that are not members of the underlying semigroup (e.g. promagma), and so on. So the real picture would be a sort of overlay of your two pictures, and maintaining it would still be tricky.

Again I agree with what you've said, but the crucial thing is that if we get that overlay wrong then to fix it we don't have to break backwards compatibility in the same way that we would if we adopt the current approach.

So then I guess one would really have just as much breaking code and maintenance anyway?

No you wouldn't. The amount of breaking code would be much less. The maintenance might be the same.

How about this as a final reason? I admit is either a weak one or a strong one depending on your perspective, but there's a reason these structures are called partiallyOrderedSemigroup rather than a semigroupicalPoset right? Namely that the algebraic structure is the most important bit, and the order is the additional structure.

[sstucki]

Also, code that depends on the base hierarchy still breaks if that changes.

That's the thing though, yes the code in the library breaks and yes the user's original algebra code breaks, but their code building the ordered structures doesn't right?

I think it does though. Because in order to show something is a preordered-X, you now need to show that it is an X first, then that it is preordered. The second half won't break, the first half will. So, unless they decide to implement everything twice (and not use the derived definitions/modules/proofs provided in the ordered structures), the same amount of code will break. No?

How about this as a final reason? I admit is either a weak one or a strong one depending on your perspective, but there's a reason these structures are called partiallyOrderedSemigroup rather than a semigroupicalPoset right? Namely that the algebraic structure is the most important bit, and the order is the additional structure.

Hehe, I'm not sure about that one. Some authors refer to a preordered (commutative) monoid as a (symmetric) monoidal preorder (e.g. Fong and Spivak in their Seven Sketches in Compositionality).

Look @MatthewDaggitt, I don't think there's a clear winner here, but you're the boss. You have put way more time into this library and I defer to your judgment. If you prefer the hierarchy to be layered the other way, let's fix it!

[MatthewDaggitt]

Look @MatthewDaggitt, I don't think there's a clear winner here, but you're the boss. You have put way more time into this library and I defer to your judgment. If you prefer the hierarchy to be layered the other way, let's fix it!

Thank you, apologies always difficult to judge when to put your foot down and I don't mean to overrule your concerns. You've definitely convinced me the decision is more nuanced than I'd thought, but I still think swapping the layout is preferable. Would you be willing to change it? If not then I'm happy to put my money where my mouth is and do it myself 👍

[sstucki]

Would you be willing to change it? I

Yes. But it may take a while (I have some other obligations this week), sorry. If it's urgent, please go ahead and make the changes.

[jamesmckinna]

Any likelihood of solving this design problem (in time) for v2.0?

[sstucki]

Sorry for the inactivity on this one. I should have accepted @MatthewDaggitt offer to do the refactor. Unfortunately, I've since changed jobs, so I have even less time to work on Agda-related things.

@jamesmckinna and @MatthewDaggitt: I haven't been paying attention to recent developments of this library. Is the new design proposed by @MatthewDaggitt still relevant?

[MatthewDaggitt]

Sorry for the inactivity on this one. I should have accepted @MatthewDaggitt offer to do the refactor. Unfortunately, I've since changed jobs, so I have even less time to work on Agda-related things.

@jamesmckinna and @MatthewDaggitt: I haven't been paying attention to recent developments of this library. Is the new design proposed by @MatthewDaggitt still relevant?

Yes unfortunately I'm still convinced the current design is the wrong one. Unfortunately I don't think I have the time to push through a better design before the release of v2.0...

As, from a backwards compatability view, a design that needs to be changed is actually worse than no design, I'm going to very reluctantly open a PR removing the Algebra.Ordered subfolder before v2.0.

I'm really really sorry. I know it's super annoying to have one's work undone and I really didn't want to have to do this. However, I think it is important to get the right design in. Of course, we're still very open to subsequent PRs after v2.0 that re-add it with the new design 👍