-
Notifications
You must be signed in to change notification settings - Fork 242
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
[ refactor ] Add Data.Nat.ListAction
#2558
base: master
Are you sure you want to change the base?
Conversation
I have to say, I don't like the module name... there are other monoids on Nat (e.g. (max, 0)) whose folds we'd also want to have in the same module if we have them. |
Thanks @Taneb ! Bear in mind that I regard this PR as provisional, indeed minimal wrt not refactoring to lift out the actual Eg, I could even imagine doing that generalisation (in whatever form) downstream, and then simply deprecating this module with its 'clunky' name. perhaps I even thought that would be inevitable, so either didn't care, or actively chose, to make the name 'clunky'... on a 'build one to throw away' principle... That said, would (any of) the following be better candidate names?
Other suggestions welcome! @JacquesCarette any thoughts on this? |
As I said elsewhere, fully agree with moving these out of where they currently are. Hmm, why If it were in |
Thanks. I had the feeling that the consensus was already 'out there' (it seems to have been a recurring issue en passant for years without anyone tackling it seriously...)
Interesting... but a rather different perspective to mine (although I could agree with
So from my point of view,
Well, indeed, but that would be a generalisation beyond the scope of this v2.3-badged PR, which I've deliberately tried to keep as minimal as possible, while opening up the design/discussion space for subsequent downstream refactorings. Besides which, I suspect (strongly) that any |
Do we also want to move |
Well... actually no, not right now, but it might very well make sense to do so in downstream PRs? The focus of this PR, and the originating linked issue was for the 'problematic' UPDATED: I should probably insert the (obligatory!?) warning against PR-creep!? shout out to @JacquesCarette who is usually very hot on this, but he may also have views about the |
Hmmm... @Taneb 's comments (in one direction), and @JacquesCarette 's (a bit in another) suggest perhaps this should be refactored in terms of And indeed that |
As I said elsewhere, agree with @Taneb that those should be moved as well. Also agree that while an issue could cover moving both sets of things, doing it in smaller PRs is more to my taste. My feeling is indeed that this stuff belongs under And yes, the generalizations of this (to more general containers + algebras) absolutely should be done as a separate, downstream refactor. |
So:
Comments, as ever, welcome! |
Data.Nat.SumAndProduct
Data.Nat.ListAction
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Other than property placement, the rest looks good!
CHANGELOG.md
Outdated
|
||
* In `Data.List.Properties`: | ||
```agda | ||
sum-++ ↦ Data.Nat.ListAction.sum-++ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, I think these ought to be in Data.Nat.ListAction.Properties
. I still will want to have sum
and product
available with a decently small footprint (dependency-wise) and bundling properties with definitions defeats that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And a corresponding Base
module for the definitions?
Actually that tends not to be the case for eg All
and Any
, so perhaps not needed (certainly at this stage)?
Implements the 'provisional' v2.3 fix for #2553 .
Issues (summarising discussion below):
Data.Nat
orData.List
(or elsewhere?) UPDATED toData.Nat.ListAction
NB.:
Data.List.Properties
concerningsum-++-commute
, but now the message is... anachronistic. Wasn't sure how to deal with this properly!