[ draft ] Alternative design for sub- and quotient- (Abelian)Groups

[jamesmckinna]

Alternative to #2852 and #2854 , based on @Taneb's original design, but:

• Normal is now below Algebra.Construct.Sub.Group
• Algebra.Construct.Sub.AbelianGroups added, and are automatically Normal

Hence:

• downstream, Algebra.Module.Construct.Sub.Bimodules are automatically suitable as Ideals
• ... below Algebra.Construct.Sub.Ring
• simplifying Algebra.Construct.Quotient.Ring

The high-level differences between the two approaches mostly consist in:

• this one is more aggressively optimised than @Taneb 's original in the spirit of [DRY] what's the best way to publicly re-export properties/structure? #2391 , in terms of making large single definitions of nested records, and opening them to expose substructure
• in avoiding, wherever possible, redundant imports/type signatures solely for the sake of making explicit the types of 'implementation details', so that the resulting (public) API for the various constructions is (or at least aims to be) as abstract as possible from a client perspective
• exact location of concepts within the Algebra hierarchy, and their mutual dependency (aiming to flatten/linearise the latter, and making the former follow a more conventional inheritance based directory/sub-directory tree structure
• making the notion of 'sub-Abelian group' explicit, and using that to streamline the development of sub- and quotient- structure of richer algebras (such as Ring) which are based on an underlying (additive) Abelian group structure, which slightly alters the conceptual, as well as concrete dependency graph compared to Taneb's Add subgroups and submodules #2852 Normal subgroups and quotient groups #2854 and Add ideals and quotient rings #2855

[JacquesCarette]

I know this is just an experiment, but I'd certainly with that this IsEquivalence record was pulled out.

[jamesmckinna]

One thing that impressed me about @Taneb 's code was the extent to which, in various places, it manages to produces huge nested record blocks which nevertheless 'do the right thing'.

I've flip-flopped over the years between this style, and a much more incremental, define every sub-record at top-level, put the pieces together step-by-step style, which the library has to date favoured.

One reason (perhaps two or more!) I am now turning towards the 'one big record' style arises from #2391 :

• a single large object, suitably re-opened as public, (re-)introduces all the 'correct' substructure, moreover with the 'rectified'/'official' names, rather than trying to invent proxy names for the top-level substructure in the other style
• when any client imports the new constructions, they aren't faced with a (DRY) choice between cherry-picking the ad-hoc names (which may be the 'correct' ones), or facing a clash/choicepoint between such names and those names introduced by open of substructures

In this instance (as perhaps elsewhere...) the definition of distinct isEquivalence : IsEquivalence ... fields at top-level is starting to emerge as an anti-pattern for me: once an Algebra.Structures.IsX object is in scope, or has been defined, then isEquivalence is available as a canonical projection from that, and indeed that should be the preferred mode-of-access (via open if necessary) for a substructure which exists solely

• to export canonical names refl, sym, trans for the properties, and their derived forms
• to construct Setoids from which Relation.Binary.Reasoning.Setoid syntax may then be brought into scope
• ...

... much of which functionality/behaviour can be achieved at a higher-level of the nesting hierarchy by suitable re-organisation of the Algebra.Properties.X hierarchy #2804 #2858 etc.

[JacquesCarette]

That _ is perverse. Sure, it can be reconstructed -- so what? Record declarations serve as documentation too!

[jamesmckinna]

Thanks for "perverse"... ;-)

I surely agree that

• record declarations should be self-documenting
  but, here, I think that
• an-line comment would here do as much work in explaining why a name isn't necessary...
• ... rather than, as now, having to introduce a private manifest field defining a module (or else expose a new name for a subfield of the subgroup object), solely for the sake of projecting out the name of its Carrier.

So... at rock-bottom, I chose this design as a optimisation for space (as well as that of my cognitive load, but it seems YMMV) and like all such, doing this prematurely might be harmful.

But as with the comment above about isEquivalence, I am starting to find that when we create/open substructures of this sort, it is usually in a context in which the 'missing'/'hidden' name of the type is already in scope with another pre-existing name which is more salient in that deployment context.

So the private module name, and or that of its sub-fields, is being created solely for the purpose of documentation.

Accordingly, in this setting, I made a design choice to avoid committing to creating such an 'ephemeral' name. But an inline comment should, I think, solve this problem?

I'd still be OK if you disagreed with my above thought process (which should, in any case, be documented towards any eventual codification of a library-design philosophy ;-)), and I guess part of the point of offering an 'alternative' design for these fundamantal structures was to create an opportunity for debate around such questions.

[JacquesCarette]

eta contract?

[jamesmckinna]

Yes! In that, it is itself an eta-contraction of the original

isNormal = record { normal = λ n g → G.comm (ι n) g }

Is it harmful to have done this?

Or are you asking whether the definition could be contracted further? Perhaps, but only via one of those odd Function.Base composition operators which compose only in one argument position of an n+2-ary function, which I find obscure rather than illuminate (my point-free fu is not always as strong as it might be).

[JacquesCarette]

I'm sure this alternative design makes a lot of sense to you @jamesmckinna and to @Taneb , but since I don't have the original in mind, your description relative to it does not really inform me in any substantial way of the pros and cons of each.

i.e. could the PR description be made less relative to knowing the original, but rather have more information about both designs in the description please?

[jamesmckinna]

I think that the best answer to the above comment might be to give a more detailed commentary in the source? (See ongoing/recent commits)

I think that this is probably more portable/surveyable than a complex interweaving of the GitHub comment trail? This still seems to be a major bugbear in using git to debate alternatives, and to document discussion around such things, as we have observed in the past, elsewhere in this project.

[jamesmckinna]

A last thought on this (or two, depending on how you count; maybe it's 3/2 of a thought): either of the following would also typecheck:

Suggested change

	ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain
	ι : _ → _

or

Suggested change

	ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain
	ι : _ -- where _ = RawGroup.Carrier domain → G.Carrier