Mess around with IsSemiringWithoutOne reexports #2499

Taneb · 2024-11-13T09:30:46Z

It was missing several and had some duplicated, which was causing problems when trying to use those names

I don't know how to changelog this

It was missing several and had some duplicated, which was causing problems when trying to use those names I don't know how to changelog this

JacquesCarette

Also need a Changelog entry.

JacquesCarette · 2024-11-13T12:18:09Z

src/Algebra/Structures.agda

    ; isMonoid               to +-isMonoid
    ; isCommutativeMagma     to +-isCommutativeMagma
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    )

-  open Setoid setoid public
+  open IsEquivalence isEquivalence public


Doesn't this removal of open Setoid setoid public change the export, i.e. Carrier is no longer visible?

Yes, this is intentional - no other structure exposes Carrier, and doing so was causing issues when trying to use the corresponding bundle.

[UPDATED} ~~Indeed, no (other) Structure~~ Only IsSuccessorSet and IsMagma export setoid, but I think, on balance, that they should not. Suggest a downstream PR to look at this more closely, unless @Taneb you want to investigate this further as part of this PR?

Re: the export of setoid from IsMagma: this is used by IsGroup in this module, so can't be removed at this stage.

MatthewDaggitt · 2024-11-14T06:26:58Z

I don't know how to changelog this

I would document this as a bug fix. Noting the removal of the Carrier export and then listing the new exports.

jamesmckinna · 2024-11-15T13:53:29Z

As the author of the prior, now offending, commit, I drew attention in the discussion comments on the relevant PR to the possibility of having introduced such a bug...

... having said that, the setoid export was for a reason, and I think that the revisions here revert the relevant consequence (namely to export negated equality...), so I think I'd prefer it if instead

either Carrier is part of an explicit hiding directive when exporting setoid (open world assumption)
or, that the exports are specifically restricted via a using directive (closed world assumption, which I think @JacquesCarette favours?)

There's a meta-issue here:

the offending commit passed an approving review by the author of the present PR
the originating history of the offending commit does not seem to have been referred back to for context/rationale/explanation

This is not to throw shade either on me (for a buggy commit), or @Taneb for the fix here, but to point out that, wittingly or unwittingly, reverting prior commits may have further subsequent negative downstream consequences.

Happy to be corrected if I've misconstrued the situation here!

jamesmckinna · 2024-11-16T10:38:30Z

Allow me to correct myself, after yesterday's splurge/rant, for which I apologise. I did some more digging through the history, and the various import/export dependencies...

Summary:

indeed, I think the setoid export is a mistake, both on its face, but also because it is an example of a Structure exporting a sub-Bundle, which as @Taneb points out, happens nowhere else in the library (so is definitely a bug! sorry for introducing it...)
the relevant exports of _≉_ are already handled in Algebra.Bundles via their Raw sub-bundles, so my objections above don't stand up, either.

Hope this helps! Apologies for interruptions in the smooth running of things...

jamesmckinna

Suggest removing the export of setoid completely... but not (yet) sure what the knock-on consequences of that might be...

jamesmckinna · 2024-11-16T10:41:26Z

src/Algebra/Structures.agda

@@ -415,15 +415,22 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
    zero                  : Zero 0# *

  open IsCommutativeMonoid +-isCommutativeMonoid public
-    using (setoid)
+    using (setoid; isEquivalence)


I'd double down on @Taneb 's suggestions, and remove the setoid export entirely. As noted in my longer meta-comment, I think it's a design error for a Structure to export a sub-Bundle... one to chalk up to my relative inexperience/lack of understanding when raising and then tackling #1917 which caused all this in the first place. hey-ho!

jamesmckinna · 2024-11-16T10:42:28Z

src/Algebra/Structures.agda

    ; isMonoid               to +-isMonoid
    ; isCommutativeMagma     to +-isCommutativeMagma
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    )

-  open Setoid setoid public
+  open IsEquivalence isEquivalence public


[UPDATED} ~~Indeed, no (other) Structure~~ Only IsSuccessorSet and IsMagma export setoid, but I think, on balance, that they should not. Suggest a downstream PR to look at this more closely, unless @Taneb you want to investigate this further as part of this PR?

jamesmckinna · 2024-11-16T11:05:57Z

Suggest removing the export of setoid completely... but not (yet) sure what the knock-on consequences of that might be...

Ugh. Worse that I thought: the uniqueness properties of inverse, defined as manifest fields, in Algebra.Structures.IsGroup, rely on Algebra.Consequences.Setoid, which depends, as the name suggests, on having a Bundled Setoid, rather than the underlying IsEquivalence for access to the properties of equality. So following my suggestion (to have IsMagma not export a setoid field) would actually have a larger scale knock-on effect.

Nevertheless, I think deleting the setoid export from IsSemiringWithoutOne should be harmless?

MatthewDaggitt · 2024-11-19T02:09:26Z

Gah these algebra imports, re-exports are always nightmarish. I'm not across the exact details, but my understanding aligns with both @jamesmckinna and @Taneb in that we try to avoid structures exporting bundles.

jamesmckinna

My suggestions could be considered downstream, but I think are worth doing here as immediate consequences of the new exports you propose?

jamesmckinna · 2024-11-27T15:44:22Z

src/Algebra/Structures.agda

+  distribˡ : * DistributesOverˡ +
+  distribˡ = proj₁ distrib
+
+  distribʳ : * DistributesOverʳ +
+  distribʳ = proj₂ distrib
+


These additions make sense, but if you are going to make them, then perhaps you should re-export them downstream from eg IsRingWithoutOne via opening an isSemiringWithoutOne manifest field... etc. which might simplify those exports elsewhere, too?

jamesmckinna · 2024-12-06T16:06:24Z

@Taneb do you want me to add a CHANGELOG entry and merge this?

jamesmckinna · 2024-12-09T10:05:10Z

Lots of other merges happening right now... so CHANGELOG conflict sadly inevitable!

jamesmckinna · 2024-12-09T11:34:43Z

@JacquesCarette I think you can now approve the changes and merge?

Mess around with IsSemiringWithoutOne reexports

e8c125b

It was missing several and had some duplicated, which was causing problems when trying to use those names I don't know how to changelog this

JacquesCarette requested changes Nov 13, 2024

View reviewed changes

MatthewDaggitt approved these changes Nov 14, 2024

View reviewed changes

MatthewDaggitt added this to the v2.2 milestone Nov 14, 2024

MatthewDaggitt added the bug label Nov 14, 2024

jamesmckinna approved these changes Nov 16, 2024

View reviewed changes

jamesmckinna mentioned this pull request Nov 22, 2024

Refactor Algebra.Consequences.*? #2502

Open

jamesmckinna reviewed Nov 27, 2024

View reviewed changes

Add changelog note

4b100df

Taneb added 2 commits December 9, 2024 11:22

merge conflict

2b21e75

merge again

38c3bb6

jamesmckinna enabled auto-merge December 9, 2024 11:34

JacquesCarette approved these changes Dec 10, 2024

View reviewed changes

jamesmckinna added this pull request to the merge queue Dec 10, 2024

Merged via the queue into master with commit d38e964 Dec 10, 2024
2 checks passed

This was referenced Dec 30, 2024

[DRY] why is _≉_ defined both for Algebra.Bundles.Raw.RawX bundles, and via Setoid instances, for Algebra.Bundles.X? #2274

Open

[ refactor ] add rawSetoid manifest fields to Algebra.Bundles.Raw #2536

Merged

MatthewDaggitt deleted the IsSemiringWithoutOne-fixes branch January 3, 2025 09:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Mess around with IsSemiringWithoutOne reexports #2499

Mess around with IsSemiringWithoutOne reexports #2499

Taneb commented Nov 13, 2024

JacquesCarette left a comment

JacquesCarette Nov 13, 2024

Taneb Nov 13, 2024

jamesmckinna Nov 16, 2024 •

edited

Loading

jamesmckinna Nov 18, 2024

MatthewDaggitt commented Nov 14, 2024

jamesmckinna commented Nov 15, 2024 •

edited

Loading

jamesmckinna commented Nov 16, 2024

jamesmckinna left a comment

jamesmckinna Nov 16, 2024

jamesmckinna Nov 16, 2024 •

edited

Loading

jamesmckinna commented Nov 16, 2024

MatthewDaggitt commented Nov 19, 2024

jamesmckinna left a comment

jamesmckinna Nov 27, 2024 •

edited

Loading

jamesmckinna commented Dec 6, 2024

jamesmckinna commented Dec 9, 2024

jamesmckinna commented Dec 9, 2024

Mess around with IsSemiringWithoutOne reexports #2499

Mess around with IsSemiringWithoutOne reexports #2499

Conversation

Taneb commented Nov 13, 2024

JacquesCarette left a comment

Choose a reason for hiding this comment

JacquesCarette Nov 13, 2024

Choose a reason for hiding this comment

Taneb Nov 13, 2024

Choose a reason for hiding this comment

jamesmckinna Nov 16, 2024 • edited Loading

Choose a reason for hiding this comment

jamesmckinna Nov 18, 2024

Choose a reason for hiding this comment

MatthewDaggitt commented Nov 14, 2024

jamesmckinna commented Nov 15, 2024 • edited Loading

jamesmckinna commented Nov 16, 2024

jamesmckinna left a comment

Choose a reason for hiding this comment

jamesmckinna Nov 16, 2024

Choose a reason for hiding this comment

jamesmckinna Nov 16, 2024 • edited Loading

Choose a reason for hiding this comment

jamesmckinna commented Nov 16, 2024

MatthewDaggitt commented Nov 19, 2024

jamesmckinna left a comment

Choose a reason for hiding this comment

jamesmckinna Nov 27, 2024 • edited Loading

Choose a reason for hiding this comment

jamesmckinna commented Dec 6, 2024

jamesmckinna commented Dec 9, 2024

jamesmckinna commented Dec 9, 2024

jamesmckinna Nov 16, 2024 •

edited

Loading

jamesmckinna commented Nov 15, 2024 •

edited

Loading

jamesmckinna Nov 16, 2024 •

edited

Loading

jamesmckinna Nov 27, 2024 •

edited

Loading