Skip to content

Mess around with IsSemiringWithoutOne reexports #2499

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Dec 10, 2024
Merged

Mess around with IsSemiringWithoutOne reexports #2499

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e8c125b
Mess around with IsSemiringWithoutOne reexports
Taneb Nov 13, 2024
4b100df
Add changelog note
Taneb Dec 9, 2024
2b21e75
merge conflict
Taneb Dec 9, 2024
38c3bb6
merge again
Taneb Dec 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,13 @@ Non-backwards compatible changes

* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.

* The names exposed by the `IsSemiringWithoutOne` record have been altered to
better correspond to other algebraic structures. In particular:
* `Carrier` is no longer exposed.
* Several laws have been re-exposed from `IsCommutativeMonoid +` renaming
them to name the operation `+`.
* `distribˡ` and `distribʳ` are defined in the record.

Minor improvements
------------------

Expand Down
19 changes: 16 additions & 3 deletions src/Algebra/Structures.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

renaming
( comm to +-comm
( ∙-cong to +-cong
; ∙-congˡ to +-congˡ
; ∙-congʳ to +-congʳ
; assoc to +-assoc
; identity to +-identity
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
; comm to +-comm
; isMonoid to +-isMonoid
; isCommutativeMagma to +-isCommutativeMagma
; isCommutativeSemigroup to +-isCommutativeSemigroup
)

open Setoid setoid public
open IsEquivalence isEquivalence public
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

@jamesmckinna jamesmckinna Nov 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


*-isMagma : IsMagma *
*-isMagma = record
Expand All @@ -444,6 +451,12 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
; ∙-congʳ to *-congʳ
)

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

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

Comment on lines +454 to +459
Copy link
Contributor

@jamesmckinna jamesmckinna Nov 27, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

zeroˡ : LeftZero 0# *
zeroˡ = proj₁ zero

Expand Down
Loading