[ discussion ] alternative design for `Algebra.Structures.IsX` and `Algebra.Properties.X`

[jamesmckinna]

This is an alternative design for the Structures and Properties hierarchies under Algebra, as an experiment following on from my ~~(currently!) failed~~ attempts to find a suitable solution to #2704 ...

The main idea can be seen as:

• a finer-grained breakdown of Algebra.Structures (which now re-exports from each of its sub-modules, now embodying the previous single record entries for each IsX structure, but with a slightly different grouping of 'cognate' such things;
• a parallel hierarchy (in order to be non-breaking) of Algebra.Properties.IsX, which can now be interleaved with those under Structures, so that successively richer structures can inherit not just properties of their vanilla substructures, but their properties as well; cf. #2251 for adding new derived operations as well...
• this (should) permit the elimination altogether of Algebra.Consequences, as the relevant structural elements would then be available sur place for proving equational properties;
• Properties modules are now further able to define other IsZ substructural fields (eg. Properties.IsSemigroup can now package the Flexible and Alternative properties into fully fledged IsFlexibleMagma and IsAlternatveMagma substructures for subsequent re-export if so desired (previously, trying to do so would have led to a dependency cycle, I think; or at least, have not been considered as 'standard' admissible extensions to IsSemigroup...)
• but currently, for backwards-compatibility, there are only isY : IsY substructures defined in each Algebra.Structures.IsX, but eg. IsGroup shows what was not previously possible (except via Algebra.Group.Properties), namely to have isQuasigroup and isLoop fields defined, and hence the possibility of IsGroup also inheriting/re-exporting their Properties;
• shims in Algebra.Bundles and Algebra.Properties.X for re-packaging and export of the corresponding IsX data.

It's WIP/DRAFT, because I stopped once I had got to IsGroup, and with it the decision about how 'wide' to make that API...

Discussion welcome!

• pros: I hope are self-evident
• contras: perhaps this merely reorganises in disguise my desire to have the API of each IsX to be as wide as possible, but currently that's only in IsGroup; a spectrum of possible choices are available
• others, on either side?

NB Outstanding issues:

• my first go at parametrisation emulating the existing Algebra.Structures means that _≈_ needs to be supplied explicitly a bit too often on re-export (I hope that can easily be fixed, but later...): in particular, the build fails at the moment for this reason;
• the choice, echoing existing practice, to parametrise on a 'flat' telescope, rather than a corresponding RawX bundle, is neither here nor there, but this design would certainly fit well with #2252 , which would moreover have the advantage that the fixities could be declared in the RawX bundle, and hence inherited on opening in the IsX structure, which would make the subsequent statement of additional properties less painful wrt precedence/parsing than at present...
• with the refactoring of Structures, we could simply make each individual IsX module put together both definition and properties (but that maybe goes against accepted wisdom)
• probably many more!

Related: instead of parametrising Reasoning modules on Setoid, in favour of IsEquivalence, we could remove the anomalous setoid field inherited from IsMagma onwards precisely to facilitate manifest field definition of new equational properties cf. bootstrapping #2692 from #2688 etc.

[JacquesCarette]

This needs deep thinking. I've added it to my ToDo list -- it's not something that just fits under a casual review of recent stdlib work.

[jamesmckinna]

This needs deep thinking. I've added it to my ToDo list -- it's not something that just fits under a casual review of recent stdlib work.

Yes... hence hypothetical-rewrite ;-) And, indeed, I wrote this as a PR simply as a means to organise a large body of code for discussion... without intending that we try to settle this any time soon, unless there's real interest/support for such a redesign...