[ fix #1694 ] Add ordered algebraic structures. #1752

sstucki · 2022-04-13T18:24:59Z

This is a starting point for addressing #1694 and eventually #481 (since we need promonoids for grading).

I implemented this a while ago but never got around to submitting a PR so I refactored it to fit current stdlib conventions as best I could, but please let me know if anything looks wrong. The PR is also missing a CHANGELOG patch, but I need some advice on what to put where there. (Is there a CHANGELOG guide somewhere?)

sstucki · 2022-04-13T18:28:08Z

(BTW, I also have an implementation of residuated pomonoids and lattices, but that will need some more refactoring before it's ready to become a PR.)

MatthewDaggitt

Thanks for the PR! Looks pretty great, just a few comments. As I mentioned, I don't have much knowledge in this area of algebra so I'm trusting that the definitions are sensible. If anyone else has more knowledge, then another review would be welcome!

src/Algebra/Ordered/Structures.agda

MatthewDaggitt · 2022-04-17T09:28:53Z

src/Algebra/Ordered/Structures.agda

+
+  record IsPosemigroup (_∙_ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isPartialOrder : IsPartialOrder _≈_ _≤_


Hmm the lack of symmetry between this and IsProsemigroup is a bit off-putting. The latter uses the algebraic structure IsSemigroup as the base structure, whereas this uses the ordered structure IsPartialOrder as the base structure. Is there a good reason for this? If not I think it'd be better for them to be consistent!

Yea, I see what you mean. The reason is that you get some structure for free once you assume anti-symmetry as well. Notably, you get ∙-cong for free or really cong for any operation that is also monotone (as you noted yourself). There's a tradeoff here between adding redundant fields/assumptions to the records vs. keeping the record structure "regular". I personally prefer not to add redundant fields unless there are good technical reasons to do so (e.g. because it makes some proofs simpler). But I don't feel strongly about this, so I'm happy to discuss alternatives.

Yup, I see your point and this is exactly the reason we have Algebra.Structures.Biased which provide alternate, "easier" ways of constructing structures when you can derive some of the axioms from the others. So I'd recommend that we preserve the symmetry here, and then add this variant to Algebra.Ordered.Structures.Biased? (which is also re-exported from Algebra.Ordered for easy use).

Alright. Two questions:

Which structure do you prefer: using the algebraic structure as a base and adding what's missing from the orders, or vice-versa? (We could also add both at once, but then isEquivalence would be duplicated, which I really don't think is a good idea.)

Is there maybe a better name than Biased for this? I don't really see in which sense either version is biased. But I also don't have any good alternative suggestions, TBH...

Upon reflection, the answer to 1. is probably to go with preorders as the base since we're going to mirror the whole algebra hierarchy (starting with magmas) and build them up anyway. For the po* structures, I'll similarly start with partial orders.

using IsPreorder directly is not a good idea because it would duplicate the IsEquivalence field which you really don't want, there shouldn't be two versions of that in the same record

Agreed!

Hmm so I just wrote 3 paragraphs about why it was better with the algebra hierarchy as a base, but deleted it as I can't distinguish in my head whether I think that because the current algebra hierarchy is so hopelessly broken or whether its actually better that I way. In the end, I've decided at this moment I also don't have the time to work through all the implications (sorry future me!). Let's just keep it the way you've got it now 👍

Yea, I can totally see that there are good arguments for and against here. It's hard to know which will work out better in the end.

Out of curiosity: when you say the algebra hierarchy is broken, do you think there would be a reasonably clean fix, or is it just an impossible problem to design hierarchies like this in Agda? I mean, it does feel like we're just implementing OO/multiple inheritance manually here, but maybe my judgment is clouded from having worked in OO languages too much in the past. In any case, I'm curious to hear if you have any ideas on how things could be improved in general. Is there some discussion around this topic somewhere? E.g. in an issue?

do you think there would be a reasonably clean fix, or is it just an impossible problem to design hierarchies like this in Agda?

I think the consensus is that it's the latter. There's no good way to define diamonds compositionally without biasing them in some regards that impacts usability. I hear that Arend's implementation of record types is supposed to have gone a long way to fixing the problem.

In no particular order here are a selection of the issues discussing problems:

IsCommutativeMonoid should use IsMonoid not IsSemigroup #239

Consequences as consequences for properties, or consequences for structured sets? #455

Cleaning up the various hierarchies #876

Setoid parameter in algebra records #1238

Redundancy in ring-like structures #1617

Thanks for these pointers. I'll bookmark #1238, which contains a lot of references to relevant related work. (Thanks @JacquesCarette!) If it's not already the case, it might be nice to summarize these discussions in some sort of README.

No problem. [Sorry for the late comment, I am just now catching up to a couple of months' worth of agda-stdlib activity!]

src/Algebra/Ordered/Structures.agda

src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda

src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda

src/Algebra/Ordered/Definitions.agda

MatthewDaggitt · 2022-04-17T09:38:52Z

src/Algebra/Ordered/Definitions.agda

+open import Data.Product using (_×_)
+
+Monotonic₁ : Op₁ A → Set _
+Monotonic₁ f = f Preserves _≤_ ⟶ _≤_


Hmm I'm now wondering if these should go in Relation.Binary.Definitions instead of here?

The reason I put them here is that they involve binary/unary operations from Algebra. There are analogous Congruence definitions in Algebra.Definitions:

agda-stdlib/src/Algebra/Definitions.agda

Lines 27 to 31 in e0e5db4

Congruent₁ : Op₁ A → Set _

Congruent₁ f = f Preserves _≈_ ⟶ _≈_

Congruent₂ : Op₂ A → Set _

Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

I figured that, if these live in the Algebra hierarchy (rather than Relation.Binary), then so should Monotonic and Antitonic.

So actually _Preserves _⟶ _ and friends are from the Relation.Binary hierarchy. I think the notion of monotonic and antitonic functions make sense for any functions, rather than just those that are used in an algebraic setting right? For example f x = x ::_ is monotonic over the lexicographic ordering over lists.

That's true, but it's equally true for Congruent. I mean the only difference between Preserves, Monotone and Congruent is how they are intended to be used. Maybe adding all these anti/mono/whathever definitions is overkill and we should just use Preserves directly? (That's what I did originally, but then I figured I should probably mirror the definition of Congruent.)

That's true about Congruent. Perhaps having it in Algebra.Definitions instead of Relation.Binary.Definitions is a mistake. Nonetheless, I would really like these new monotonic definitions to live in the latter.

Another argument is that if we ever want to add a new ordered definition that used both the order and the equality relation, then this module's current module-level arguments wouldn't allow that.

OK, so just to double check before making the changes:

I'll move all the definitions from Algebra.Definitions.Ordered to Relation.Binary.Definitions then.

I'll drop the use of Op from Algebra.Definitions (to make the definition generic, and avoid cycles in the module imports).

I'll keep {Mono,Andt}tonic even though they will be essentially aliases of Preserves.

Agreed?

Sounds good 👍

MatthewDaggitt · 2022-04-17T09:41:31Z

The PR is also missing a CHANGELOG patch, but I need some advice on what to put where there. (Is there a CHANGELOG guide somewhere?)

There isn't a guide I'm afraid.

new modules should be listed under the "New modules" section
new additions to existing modules should be added in the appropriate place under the "Other minor changes" section.

sstucki · 2022-04-19T10:23:09Z

Thanks for the review @MatthewDaggitt. I'll update the PR to address the obvious stuff, but I think some points warrant further discussion. In particular, I'm not an algebraist either. I mechanized this stuff a while back because I needed it for my experiments with graded (co)monads. Maybe @andreasabel, @JacquesCarette or @Taneb, who are part of the discussion in #1694 have some additional comments and ideas?

sstucki · 2022-04-19T10:59:39Z

Oh, and @laMudri too!

Taneb · 2022-04-19T11:05:23Z

I'll take a look this evening!

Taneb

I'd like to see some proofs in Data.Nat.Properties giving examples of these structures, too, but that could be in a later PR

src/Algebra/Ordered/Bundles.agda

sstucki · 2022-04-20T07:16:17Z

Adding example properties about Nat (as @Taneb suggests) should be easy since all the ingredients are already there. @MatthewDaggitt, would you prefer having these in the current PR or a separate one?

Also: does anyone know if it's possible to create a PR based on another one without the changes from the first PR showing up in the first one? I like to split PRs into manageable chunks but it kinda defeats the point if everything just gets lumped together anyway...

MatthewDaggitt · 2022-04-20T08:05:35Z

Adding example properties about Nat (as @Taneb suggests) should be easy since all the ingredients are already there. @MatthewDaggitt, would you prefer having these in the current PR or a separate one?

Happy to have them added to this one. They're conceptually part of the same addition to the library, and it's always a good sanity check to actually use things after they've been defined to check there aren't any unforeseen wrinkles.

Also: does anyone know if it's possible to create a PR based on another one without the changes from the first PR showing up in the first one? I like to split PRs into manageable chunks but it kinda defeats the point if everything just gets lumped together anyway...

Not easily. The only way I could think of for not having the changes in the 1st PR show up in the 2nd PR without having the merged the 1st one is making a PR against your original PR rather than the master branch. But I don't think you can do such a thing on this repo, only your own fork?

sstucki · 2022-04-20T19:42:31Z

The updated PR now contains example properties about Nat (as suggested by @Taneb). The corresponding definitions/proofs of the ordered structures and bundles replace the earlier (unordered) versions, which are now available as re-exported definitions from the ordered modules (to remain backwards-compatible). This is to avoid code duplication. If, for some reason, you prefer to keep the old hand-coded versions nevertheless, I can add them back.

MatthewDaggitt · 2022-04-21T09:27:55Z

Apologies, I didn't realise your changes to Data.Nat.Properties were going to involve anything but additions. Could we leave the Data.Nat.Properties changes to a separate PR?

MatthewDaggitt · 2022-04-21T09:29:06Z

By the way thank you for your patience with this @sstucki, I realise it's a lot of refactoring. The design decisions are complicated, and definitely best to try and get them right now.

sstucki · 2022-04-21T10:43:39Z

Apologies, I didn't realise your changes to Data.Nat.Properties were going to involve anything but additions. Could we leave the Data.Nat.Properties changes to a separate PR?

OK, I'll factor this into a separate PR then.

laMudri

Looks good! In the long run, I think we need a better approach to generating these definitions, but this is probably the best we can do for now.

laMudri · 2022-04-22T08:01:40Z

src/Algebra/Ordered/Structures.agda

+  open IsPartialOrder isPartialOrder public
+
+  ∙-cong : Congruent₂ ∙
+  ∙-cong = mono₂⇒cong₂ _≈_ _≈_ Eq.sym reflexive antisym mono


There's always an argument with these derived properties that they should appear in an auxiliary constructor rather than in the main record. In this case, I'm not really sure; I think we often have a proof of ∙-cong lying around anyway, but maybe we don't actually gain anything from putting it in because we never really have to look at these proof terms. This could come up if we want to take the opposite ordering and have that be a definitional involution, but maybe because mono should stay the same, ∙-cong does too.

Yes, I was thinking along the same lines. @MatthewDaggitt actually suggested a different design where the algebraic structures (rather than the orders) are used as a base, and then there's a better case for keeping cong and adding the type of constructors you mention (see our discussion further up in the thread). I'd be curious to hear which design you'd prefer.

src/Algebra/Ordered/Bundles.agda

src/Algebra/Ordered/Structures.agda

laMudri · 2022-04-22T08:14:21Z

src/Algebra/Ordered/Structures.agda

+  field
+    isPreorder  : IsPreorder _≈_ _≤_
+    ∙-cong      : Congruent₂ ∙
+    mono        : Monotonic₂ ∙


It'd be nice to have monoˡ and monoʳ, too, like for cong.

Good point, will add those! 👍

Uh, now I'm confused. The type of congˡ is LeftCongruent which actually states that the operation is congruent in its second, i.e. right argument. And similarly for RightCongruent. Is that a bug? Or some special meaning of "left" and "right" that I'm missing?

agda-stdlib/src/Algebra/Definitions.agda

Lines 33 to 37 in 650e05f

LeftCongruent : Op₂ A → Set _

LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_

RightCongruent : Op₂ A → Set _

RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_

Also, I'm not a huge fan of left/right because it doesn't generalize to n-ary operations. How about mono₁ and mono₂?

Hmm, yeah, I'd have thought congˡ had type ∀ {x x′ y} → x ≈ x′ → x ∙ y ≈ x′ ∙ y too. I can justify the current naming as saying that left-multiplication (by x) preserves equivalence, but when I'm using it in a proof, I don't think I'd think that way. IIRC, there's a similar problem with distributivity or zero, where one is the reverse of the other (something like LeftZero means 0 * x ≈ x but LeftDistributive means x * (y + z) ≈ x * y + x * z, or vice versa).

As for numbers, I guess it side-steps any existing naming conventions, but introduces the problem of needing to choose between being 0-based or 1-based. I think (3+n)-ary operations are very rare in algebra, so I'm not too worried about that potential generalisation.

OK, I can see that someone might have had good reasons to name {Left,Right}Congruent the way they did and I don't want to break backwards compatibility, so I'll not "fix" this unless @MatthewDaggitt tells me to. As for the mono variants, I'll go with mono₁ and mono₂ instead of for monoˡ and monoʳ for now, mostly because I don't know whether to follow that strange backwards terminology or not. (Again, unless @MatthewDaggitt tells me otherwise.)

sstucki · 2022-04-22T08:58:21Z

Thanks for your input @Taneb and @laMudri!

sstucki · 2022-04-26T08:20:52Z

By the way thank you for your patience with this @sstucki, I realise it's a lot of refactoring.

Well, thank you for your patience @MatthewDaggitt, and for all your hard work on the Agda stdlib and for the community in general — much appreciated!

sstucki · 2022-04-26T08:31:56Z

@MatthewDaggitt and @Taneb: the changes to Data.Nat.Properties are now living in a separate branch: https://github.com/sstucki/agda-stdlib/tree/nat-ordered
I'll submit the corresponding PR once this one has been merged.

sstucki · 2022-04-26T11:40:10Z

I think I have now addressed all the open requests for changes. I hope I didn't miss anything, as there have been quite a few discussions going on in parallel. 😅 (Thanks to all involved!)

sstucki · 2022-05-02T07:50:31Z

@MatthewDaggitt, is there anything more you need me to do here?

MatthewDaggitt · 2022-05-02T08:20:11Z

Sorry for the delay. Merging in!

Thanks again for the great PR @sstucki!

MatthewDaggitt · 2022-05-02T08:22:27Z

I should add that if you are planning to make the changes to Data.Nat.Properties in a separate PR, can we make the changes add the new structures only rather than refactor everything to define the new structures first and then extract the old structures later? I know it would be less code, but I think we would lose a significant amount of readability and maintainability.

sstucki · 2022-05-02T08:35:43Z

Sorry for the delay. Merging in!

Thanks for all the help @MatthewDaggitt!

I should add that if you are planning to make the changes to Data.Nat.Properties in a separate PR, can we make the changes add the new structures only rather than refactor everything to define the new structures first and then extract the old structures later? I know it would be less code, but I think we would lose a significant amount of readability and maintainability.

I have already prepared the changes for the PR in a separate branch (just separated them out from what was in this PR earlier). I'm afraid, it does precisely what you ask me not to do. 😓 If it's OK with you, I'll submit the PR as is anyway, and if the readability/maintainability is indeed worse, I'll refactor it to keep as many of the old proofs as possible. Does that sound OK?

sstucki force-pushed the algebra-ordered branch 2 times, most recently from e2dcf11 to e0e5db4 Compare April 13, 2022 18:33

MatthewDaggitt reviewed Apr 17, 2022

View reviewed changes

MatthewDaggitt added addition status: being-worked-on labels Apr 17, 2022

MatthewDaggitt added this to the v2.0 milestone Apr 17, 2022

MatthewDaggitt reviewed Apr 17, 2022

View reviewed changes

sstucki force-pushed the algebra-ordered branch from e0e5db4 to 4cbd95e Compare April 19, 2022 12:29

Taneb requested changes Apr 20, 2022

View reviewed changes

src/Algebra/Ordered/Bundles.agda Outdated Show resolved Hide resolved

sstucki force-pushed the algebra-ordered branch from 4cbd95e to b3da48f Compare April 20, 2022 19:28

MatthewDaggitt added the library-design label Apr 21, 2022

laMudri reviewed Apr 22, 2022

View reviewed changes

sstucki force-pushed the algebra-ordered branch from b3da48f to b24b76d Compare April 22, 2022 11:56

sstucki force-pushed the algebra-ordered branch from b24b76d to 594f239 Compare April 26, 2022 08:28

sstucki added a commit to sstucki/agda-stdlib that referenced this pull request Apr 26, 2022

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

fb9f04c

sstucki force-pushed the algebra-ordered branch from 594f239 to 272f0b2 Compare April 26, 2022 10:54

sstucki added a commit to sstucki/agda-stdlib that referenced this pull request Apr 26, 2022

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

53dd4ef

[ fix agda#1694 ] Add ordered algebraic structures.

db85aa3

sstucki force-pushed the algebra-ordered branch from 272f0b2 to db85aa3 Compare April 26, 2022 11:00

Added missing CHANGELOG entries

2ca716f

MatthewDaggitt added status: ready and removed status: being-worked-on labels May 2, 2022

MatthewDaggitt merged commit cadca35 into agda:master May 2, 2022

sstucki added a commit to sstucki/agda-stdlib that referenced this pull request May 2, 2022

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

2c9232b

sstucki deleted the algebra-ordered branch May 2, 2022 08:35

sstucki mentioned this pull request May 2, 2022

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

Closed

andreasabel mentioned this pull request Jul 24, 2023

Put indexed data types in the right universes #2030

Merged

andreasabel mentioned this pull request Aug 27, 2023

ghc 9.8 #2074

Merged

andreasabel mentioned this pull request Oct 12, 2023

Bump Haskell CI (fork) to latest GHC versions #2142

Closed

	Congruent₁ : Op₁ A → Set _
	Congruent₁ f = f Preserves _≈_ ⟶ _≈_

	Congruent₂ : Op₂ A → Set _
	Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

	LeftCongruent : Op₂ A → Set _
	LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_

	RightCongruent : Op₂ A → Set _
	RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_

[ fix #1694 ] Add ordered algebraic structures. #1752

[ fix #1694 ] Add ordered algebraic structures. #1752

Conversation

sstucki commented Apr 13, 2022

sstucki commented Apr 13, 2022 • edited Loading

MatthewDaggitt left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MatthewDaggitt commented Apr 17, 2022

sstucki commented Apr 19, 2022

sstucki commented Apr 19, 2022

Taneb commented Apr 19, 2022

Taneb left a comment

Choose a reason for hiding this comment

sstucki commented Apr 20, 2022

MatthewDaggitt commented Apr 20, 2022

sstucki commented Apr 20, 2022

MatthewDaggitt commented Apr 21, 2022

MatthewDaggitt commented Apr 21, 2022

sstucki commented Apr 21, 2022

laMudri left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sstucki commented Apr 22, 2022

sstucki commented Apr 26, 2022

sstucki commented Apr 26, 2022

sstucki commented Apr 26, 2022

sstucki commented May 2, 2022

MatthewDaggitt commented May 2, 2022

MatthewDaggitt commented May 2, 2022

sstucki commented May 2, 2022

sstucki commented Apr 13, 2022 •

edited

Loading