Skip to content

Move "raw" bundles to Data.X.Base #1755

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.

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

Closed
MatthewDaggitt opened this issue Apr 21, 2022 · 7 comments · Fixed by #1810
Closed

Move "raw" bundles to Data.X.Base #1755

MatthewDaggitt opened this issue Apr 21, 2022 · 7 comments · Fixed by #1810

Comments

@MatthewDaggitt
Copy link
Contributor

Currently the raw bundles, e.g. RawMagma are defined in Data.X.Properties but they should really be defined in Data.X.Base as they don't require any properties.

@JacquesCarette
Copy link
Contributor

Except that I see that this makes Data.X.Base now depend on Algebra.Bundles. That's not too too heavyweight, but do we want Data.X.Base to have quite so much in it? I'd prefer Data.X.Bundles, now that I look at the details of #1810 .

@Taneb
Copy link
Member

Taneb commented Sep 5, 2022

I'd rather something like a new module Algebra.RawBundles or Algebra.Bundles.Raw containing the definitions of the raw bundles, which can be imported at much lower cost from Data.X.Base

@JacquesCarette
Copy link
Contributor

But that would still leave Data.X.Base to depend on Algebra.Bundles if those are actually imported.

Won't Algebra.RawBundles (or equivalent) grow to something really large, as it would depend on all algebras? I certainly think that having these be defined in a module that mentions X in its name would help.

@Taneb
Copy link
Member

Taneb commented Sep 5, 2022

I think I didn't explain myself right. I meant that the definition of the types RawMagma, RawMonoid, RawGroup, etc, be moved into the new module Algebra.RawBundles, and then Data.X.Base can import Algebra.RawBundles and we define X-rawGroup in Data.X.Base.

@MatthewDaggitt
Copy link
Contributor Author

I agree with @Taneb (and would vote for Algebra.Bundles.Raw)

@Taneb Taneb assigned Taneb and unassigned Taneb Sep 20, 2022
@Taneb
Copy link
Member

Taneb commented Sep 20, 2022

I'm going to try to make a PR this evening moving the definitions of RawX to Algebra.Bundles.Raw

@5xy1
Copy link
Contributor

5xy1 commented Sep 20, 2022

@Taneb Maybe I could help with this? I can update my PR today.

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Oct 24, 2022
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Oct 25, 2022
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Oct 26, 2022
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Oct 30, 2022
@andreasabel andreasabel mentioned this issue Aug 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants