search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Refactor `Algebra.Solver.*Monoid` #2407

Closed jamesmckinna closed 4 weeks ago

jamesmckinna commented 3 months ago

Fixes #2403

NB:

jamesmckinna commented 3 months ago

Converted to DRAFT for further refactoring... and now back again.

jamesmckinna commented 3 months ago

I'd converted back to draft with a view to more drsatic refactoring, but then lost my nerve over the knock-on consequences for deprecation/backwards-compatibility, so I'll leave those for another time a breaking PR for v3.0... ;-)

And in the meanwhile: merge conflict hell!

jamesmckinna commented 3 months ago

Will leave the CHANGELOG until after v2.1... and DONE: update deprecation warnings to v2.2!

jamesmckinna commented 2 months ago

A couple of minor improvements suggested.

On a bigger scale: this seems like a lot of duplication. Feels like one could abstract over the differences between CommutativeMonoid/Normal and IdempotentCommutativeMonoid/Normal instead of this copy-pasta. But that's an easy comment for me to make!!! I should actually try it.

For sure, the duplication was already there in the library. This PR merely refactors it to make it evident, so in that sense this PR should be regarded as 'provisional', even if mergeable. The Normal type family in each case is Vec M for M the carrier of a suitable Monoid, with the homomorphism properties being generic, so yes, with more work, I'm sure it could be made more streamlined. Your zipWith comment is very helpful in pointing the way...

The downstream refactoring alluded to in the preamble of #2403 would spruce up the homomorphism correctness proof machinery, but at the cost, again, of having to re-export stuff, now from a different, but again shared, module/record (I've experimented with this already, but fresh eyes might be welcome! UPDATED: see below), else have a heavier-weight move/rename-plus-deprecate refactoring, which I just couldn't face right now.

But happy to reconsider, and mark as DRAFT, pending further refactoring requiring a bit more intelligence/insight.

BTW, part of the purpose of this PR, ahead of tackling the more intricate complexities of Tactic.MonoidSolver and Tactic.RingSolver, is indeed to consider adding Algebra.Solver.AbelianGroup, in which the algebra of Normal forms is again that of zipWith _+_, but on vectors of integers. It seems as though this might be (part of) the missing piece of the jigsaw around Tactic.RingSolver seemingly be(hav)ing 'not quite right' when coefficients in the ring sum to zero... cf. #1116 / #1769

jamesmckinna commented 2 months ago

Latest commits removes dependency on Data.Nat.GeneralisedArithmetic.fold in favour of Algebra.Definitions.RawMonoid._×_ cf. #2446 towards identifying common structure in the Commutative/IdempotentCommutative monoid case of Normal...

jamesmckinna commented 2 months ago

@JacquesCarette you wrote:

On a bigger scale: this seems like a lot of duplication. Feels like one could abstract over the differences between CommutativeMonoid/Normal and IdempotentCommutativeMonoid/Normal instead of this copy-pasta. But that's an easy comment for me to make!!! I should actually try it.

See Algebra.Solver.*Monoid.* refactoring on branch jamesmckinna:new-solver-refactor for a first second go in this direction... but one which plays a bit more fast-and-loose about the various exported names...

JacquesCarette commented 1 month ago

This looks good to me.

I tried to find the second refactor on the branch you pointed to, but I wasn't quite sure what to look at (i.e. which commits are for this?). Maybe make a tentative PR for that as well, to make it easier to review?

jamesmckinna commented 1 month ago

Given the additional subtleties involved in pursuing your further ideas regarding refactoring in #2457 , does it make sense to aim to merge this in the meantime?

JacquesCarette commented 1 month ago

[...] does it make sense to aim to merge this in the meantime?

As long as the additional refactor doesn't introduce compatibility issues, then yes, it makes sense to merge this in first.

jamesmckinna commented 1 month ago

[...] does it make sense to aim to merge this in the meantime?

As long as the additional refactor doesn't introduce compatibility issues, then yes, it makes sense to merge this in first.

Well, that's a good question! I guess that the NormalAPI is nowhere exposed as such in the (existing) 'top level' Algebra.Solver.*Monoid modules, so as long as we feel free to change that API under the abstract Tactic interface, it should be OK, right?

Or not!?

jamesmckinna commented 1 month ago

And... as for "compatibility issues", I think there won't be any arising from #2457 ... given the (relative) care taken to preserve (even if to deprecate) the v1.*/v2.1 API ...

MatthewDaggitt commented 1 month ago

After those are addressed, we should definitely merge!

jamesmckinna commented 1 month ago

@MatthewDaggitt thanks for the very detailed feedback. Summarising:

@JacquesCarette Against the discussion on #2457 , which I think can follow-on downstream, I still think this is worth merging now, as a refactoring-with-deprecations. The rest can follow later?

jamesmckinna commented 4 weeks ago

Thanks @MatthewDaggitt for resolving the merge conflict... I'd have got there once I'd woken up... ;-)

jamesmckinna commented 4 weeks ago

Apologies for inaccuracy in my summary of changes: it seems as though I did in fact make the breaking change of making the module R private in Algebra.Solver.Monoid.Solver, so it's not now exported publicly from Algebra.Solver.Monoid.

I've suggested on the downstream issue #2472 that we take no action on this (until eg. a release candidate for v2.2?), but advice/counter-suggestions welcome!