The free Magma on a Set, resp. Setoid [bis]

[jamesmckinna]

Clean version of #1954 .

UPDATED: I'd like to push ahead with this instance, and others, but I'm now starting to worry about where they should live:
Algebra.Bundles.Free.X or Algebra.Free.X? or somewhere else?

[JacquesCarette]

Looking good!

I can definitely see how to generate the vast majority of this (given just a few user-provided names).

[MatthewDaggitt]

Hmm I'm a little bit unsure of all these complicated named and unnamed submodules. Generally when they appear it means we haven't got the organisation quite right. It also makes it harder for the user to understand what's in scope at any given point in time.

I wonder how we can simplify it? While doing so we should consider how the organisation will be extended when encoding the free variants of more complicated structures.

I'm now starting to worry about where they should live:
Algebra.Bundles.Free.X or Algebra.Free.X? or somewhere else?

Definitely prefer Algebra.Free.X

[jamesmckinna]

Many thanks for all the very helpful and constructive review suggestions, esp. wrt use of private modules. I thinkthat I shouldn't try to add any more to this for now.

UPDATED: now added use of Identity and Composition for MagmaHomomorphisms.

[jamesmckinna]

@MatthewDaggitt

Definitely prefer Algebra.Free.X

I agree, and moved things accordingly.

[jamesmckinna]

Hmm I'm a little bit unsure of all these complicated named and unnamed submodules. Generally when they appear it means we haven't got the organisation quite right. It also makes it harder for the user to understand what's in scope at any given point in time.

I wonder how we can simplify it? While doing so we should consider how the organisation will be extended when encoding the free variants of more complicated structures.

So... I agree. I think (and hope!) that the use of private modules, and reverting to a more standard naming scheme, now means that the scoping is (much) easier to grasp.

But as for the use of nested modules in general, I personally do find it easier to use them to help localise/focus my thinking. And since the constructions are, categorically, unique 'up to', I've definitely found it helpful to keep the various appeals to Existence and Uniqueness separate, and local.

[jamesmckinna]

Can we (now) merge this, please?

[JacquesCarette]

As stand-alone code, this is great.

But this also represents a non-trivial new design, and there's various things I am not so sure about. I don't want to merge this in right now, just to have a backwards compatibility problem in 3 months from now.

In places, this code seems really quite verbose (and that might be inevitable). And it might benefit quite a lot from the vapourware of a merge of parts of agda-categories into stdlib. And shrink too.

So I don't feel like pushing the 'merge' button. I wouldn't be upset of someone else did - I just don't want to be the one to commit this design to the library!

[jamesmckinna]

I'll wait until the discussion concludes on whether to merge at all, and then fix up whatever CHANGELOG conflicts there are at that point.

UPDATED: That said, if not merged (or, in any case!?), then it's probably worth lifting out those commits defining the Bundled Homomorphism constructions as a separate PR addressing #1960 ... see #2383

[jamesmckinna]

OK, a year has gone by, and even the one positive review is... unclear whether this should be merged.

I think it's worth pulling out the bundled Homomorphism commits, and trying to get those merged, ahead of returning to this one... but when? May 2025? :-(

[JacquesCarette]

I agree that splitting off the immediately mergable stuff into a separate PR is a good idea. As to the rest, you'll need to explicitly prod some not-me reviewers into action.

[jamesmckinna]

Marking as blocked-by-issue until #2383 (and possibly others!?) get completed and merged... and a CHANGELOG merge conflict takes care of worrying about needing to review the rest... ;-)

[jamesmckinna]

Converting back to DRAFT:

• the CHANGELOG is too bit-rotted (pre-v2.0!)
• the dependency on (the fruits of) Add bundled homomorphisms #2383 should be made explicit/refactored after any eventual merge of that PR
• the design should be further discussed (somewhere... where!?) before proceeding, but so far only @JacquesCarette has engaged with that, and then to express scepticism about the particular choices made here

This PR was only ever intended as a prototype/template for adding all manner of Free algebraic constructions, but if we can't agree on Magma, then perhaps it's only worth revisiting at some later point in time (despite eg #2407 and its antecedents/descendants being based on various implementations of FreeMonoid... one Fin-based, as here, the other in Tactic.MonoidSolver in 'functorial' style).

[JacquesCarette]

So I think we should implement a few more FreeX to shake out the design space. Have a student who could, given a list of things to try.

[jamesmckinna]

So I think we should implement a few more FreeX to shake out the design space. Have a student who could, given a list of things to try.

@JacquesCarette that would be great:

• FreeGroup (and, in proof-relevant guise, to normalising/Solver architecture for compiling equational proofs Optimising Setoids/reasoning by 'rewriting' otherwise higher-dimensional equalities #2629 )
• FreeAbelianGroup (we're missing Solver for Integer!)
• Free(Commutative)Ring

In each case, there's (morally) also a connection with the associated Solver architecture(s), and more generally, the choice between 'Free X' and 'Free extension of X'... so plenty of space for a student to explore!

[JacquesCarette]

One could also envisage

• FreeSemigroup (non-empty lists)
• FreeLeftZeroSemigroup (aka 'First')
• FreeRightZerosemigroup (aka Last)
• FreeMonoid (!)

since they all have normal forms.

FreeGroup is tricky as it is quite different from FreeMagma and FreeMonoid: the latter have normal forms, but FreeGroup doesn't. So it feels like a completely different kettle of fish for which we don't really have a prototype.

[jamesmckinna]

What's the relationship between Free(Abelian)Group and FreeZModule (suitably understood in the noncommutative case)?

[JacquesCarette]

What's the relationship between Free(Abelian)Group and FreeZModule (suitably understood in the noncommutative case)?

Good question - I don't know! Of course, Z-Modules and Abelian Groups are 'the same thing', but no idea how that lifts to Free.

[JacquesCarette]

Apparently they are the same.

[jamesmckinna]

See also #2695 (comment) and perhaps we should move the discussion back to #2539 to record the various choices, compared to any particular PR such as this.