Skip to content
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

[DRY] refactor #2479 #2485

Merged
merged 2 commits into from
Sep 28, 2024
Merged

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Sep 26, 2024

This refactors the (very!) recent additions to Data.List.Membership.Propositional.Properties for nested lists in favour of delegation to existing functionality.

NB:

  • I should have seen this during my review of Lists: porting several lemmas from other libraries #2479 , but ... l'esprit de l'escalier, I guess ;-)
  • the deprecation of map∷-decomp is possibly redundant/excessive, given how recently introduced was that name/definition
  • the newly introduced replacement name/definition map∷⁻ is likewise arguably redundant, in favour of inlining its definition, but useful perhaps for its type which enforces the variable = complex refinement of our existing heuristic for writing library rewrite lemmas in the form complex = simpler
  • I have only done a back-of-the-envelope analysis to conjecture that the refactored definitions have the same computational behaviour esp. wrt strict-/lazi-ness as the originals, but separate confirmation might be welcome!

I'd be happy either way if this were merged or not, but it struck me as a useful reminder to be careful (and: more careful than I had been) about reviewing contributions against possible DRY violations.

@Taneb
Copy link
Member

Taneb commented Sep 26, 2024

If something's only just been introduced, and hasn't actually been released yet (2.2 is still "in development"), it definitely doesn't need a deprecation, it can just be removed

@jamesmckinna
Copy link
Contributor Author

If something's only just been introduced, and hasn't actually been released yet (2.2 is still "in development"), it definitely doesn't need a deprecation, it can just be removed

Yes, that was my original thinking, but as @omelkonian 's contribution was based on existing external libraries, it occurred to me that there are pre-existing client uses of these 'new' definitions... so such uses perhaps 'deserve' the deprecation warning?

But if @omelkonian were to refactor those external libraries in the meantime... it would definitely make sense to streamline this PR even further!

@omelkonian
Copy link
Contributor

@jamesmckinna There is no need to care about such deprecation warnings, since these are not 'external libraries' per se; one is my personal prelude and another is a verification project that is not meant to be imported at all.

@jamesmckinna
Copy link
Contributor Author

It occurs to me that corresponding lemmas ought to be provable in the Setoid case... but I run up against problems with level polymorphism when attempting this. @omelkonian did you try this at any point?

@JacquesCarette
Copy link
Contributor

If something's only just been introduced, and hasn't actually been released yet (2.2 is still "in development"), it definitely doesn't need a deprecation, it can just be removed

Strong agree: the kind of entropy you build in if you're that strict reduces development to a crawl.

@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Sep 28, 2024
@JacquesCarette JacquesCarette added this pull request to the merge queue Sep 28, 2024
Merged via the queue into agda:master with commit 7e94c15 Sep 28, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants