Refactor Algebra.Solver.*Monoid (further!)

[jamesmckinna]

Following a suggestion by @JacquesCarette on #2407 . Also fixes #2403

NB.

• updates/'rectifies' the syntax for Expr as backquoted versions of the RawMonoid signature; deprecates the 'old' syntax
• 'provisional'/'tentative'/'DRAFT' for review/comparison with above PR
• no CHANGELOG, but would be substantially that of above PR

This perhaps represents the "subsequent downstream refactoring" alluded to in that PR, at least as regards further improving the 'shared' interface offered/afforded by the API for Normal terms... for the cost of supplying IsMonoid and IsMonoidHomomorphism proofs upfront.

Possibly a 'better' version to go for straightaway rather than going via 'transitional' #2407 ? (NB. If so, need to cherry pick the other tweaks to the various related Solver modules...)

[JacquesCarette]

Nice.

But what I really meant was that at least CommutativeMonoid/Normal and IdempotentCommutativeMonoid/Normal are special cases of a single normal form over a ring. So those two pieces of code can be merged.

Also, in Monoid/Normal, while you define NF as a (raw) Monoid, you don't use that anywhere. In fact, lower down, you use the list explicitly, instead of taking the information out of the NF that you've just defined.

[jamesmckinna]

@JacquesCarette you wrote:

But what I really meant was that at least CommutativeMonoid/Normal and IdempotentCommutativeMonoid/Normal are special cases of a single normal form over a ring. So those two pieces of code can be merged.

Oh, I think that I didn't yet see that commonality, only that they share some structure in common, but the zipWith combiner defining the monoid operation on normal forms is different in each case (corresponding to a different underlying Monoid that Vec is taking a free thing over... but maybe that's part of your Ring structure??? (UPDATED: I thought it was something more like a wreath product of a free monoid based on List/Vec with an underlying monoid given by ℕ in the commutative case (bag multiplicity) and Bool in the idempotent commutative case (set inhabitation)... but happy to be shown a better analysis!)

UPDATED: In other words, there should be a construction in Data.Vec.Properties (Or in CommutativeMonoid.Normal? why doesn't this work for Monoid.Normal, too?) that, given a Monoid M, then exhibits Vec n M.Carrier as carrying an IsMonoid structure with identity element ε = replicate n M.ε and operation _•_ = zipWith M._∙_... and given a generator (or merely an element?) m of M.Carrier, injects var i into Vec n M.Carrier as the vector whose i th component is m, and M.ε otherwise... ie. 'm times the basis vector e_i' as it were...?

Also, in Monoid/Normal, while you define NF as a (raw) Monoid, you don't use that anywhere. In fact, lower down, you use the list explicitly, instead of taking the information out of the NF that you've just defined.

Also true (I think)... except that in this refactoring, do I not (implicitly) invoke the monoid operation as being given by the _++_ operation of ++-[]-isMonoid... so yes, I could drop the 'correct' symbol in place I suppose (a use/mention sense/denotation distinction?) UPDATED: latest commit does that now!

NB. Also, I am only refactoring by re-using existing code that was already there... without (much) attempt to exploit it for 'better' proofs, more like doing a grandiose CSE on the whole thing... so there's (obviously) potentially still room for improvement!

[jamesmckinna]

Re: discussion of potential Ring common generalisation above.

I guess what I can now glimpse is that the construction above of the form

UPDATED: In other words, there should be a construction in Data.Vec.Properties (Or in CommutativeMonoid.Normal? why doesn't this work for Monoid.Normal, too?) that, given a Monoid M, then exhibits Vec n M.Carrier as carrying an IsMonoid structure with identity element ε = replicate n M.ε and operation _•_ = zipWith M._∙_... and given a generator (or merely an element?) m of M.Carrier, injects var i into Vec n M.Carrier as the vector whose i th component is m, and M.ε otherwise... ie. 'm times the basis vector e_i' as it were...?

should better be phrased in terms of a Semiring, in the one case, the Nat version, and in the other with the Bool version (where _+_ = _∨_ and _*_ = _∧_ with 0# = false and 1# = true...

Is that what you were intending?

[JacquesCarette]

Yes!

[jamesmckinna]

Going back to DRAFT while I figure out the Semiring argument... and subsequent refactoring in the light of it.

And a bit more further thought suggests that the construction at hand is most general when presented with one Monoid acting by multiplication on another (additive) CommutativeMonoid... so only a Semiring when the carriers coincide... Or am I missing something fundamental?

UPDATED: I'm finding this a bit hard to get my head round (esp. why is the Monoid case different in its underlying structure of Normal forms different from the common Commutative case?), so definitely think I/we should focus effort first on #2407 until/unless I can sort out the details of this one. And right now, that seems unlikely in the short term. At least, it seems as though a lot more Algebra.Action.* infrastructure (incl. #2450 ) wants to be developed first?

[JacquesCarette]

Might be best to not worry about Semiring for now? Perfect is the enemy of progress or some such.

[jamesmckinna]

Might be best to not worry about Semiring for now? Perfect is the enemy of progress or some such.

But still: are you suggesting to go via #2407 , or via the more elaborate refactoring here?

[JacquesCarette]

I prefer this one.

[jamesmckinna]

I prefer this one.

Given @MatthewDaggitt 's endorsement of #2407 I'm going to suggest that we go with that one for now, and then follow-up with this one once the infrastructure is in place to fulfil the Semiring-action refactoring.