[DRY] refactor #2479 - Githubissues

jamesmckinna commented 2 months ago

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 #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 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

@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 commented 2 months ago

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 commented 2 months ago

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.

agda / agda-stdlib

[DRY] refactor #2479 #2485