Refactor `Algebra.Solver.*Monoid`

[jamesmckinna]

Fixes #2403

NB:

• for backwards compatibility, each module exports the Expr API publicly (but not the new API for Normal forms)
• module Monoid.Tactic adopts the API for *CommutativeMonoid, but maybe the Monoid.prove type should standardise on this as well?
• misc. tweaks to existing other Solver modules

[jamesmckinna]

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

[jamesmckinna]

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]

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

[jamesmckinna]

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]

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]

@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]

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]

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]

[...] 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]

[...] 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]

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]

After those are addressed, we should definitely merge!

[jamesmckinna]

@MatthewDaggitt thanks for the very detailed feedback. Summarising:

• I've fixed the newly-introduced module exports to hopefully now not introduce new names, but the original export of module R in Algebra.Solver.Monoid is legacy, so leaving it for now.
• I've done the suggested deprecations and updated CHANGELOG
• I changed the Tactic module name to Solver as a pro tem measure, Proof(s) seemed ... not quite right? Implementation feels too... generic?

@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]

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

[jamesmckinna]

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!