[DRY] why is `_≉_` defined both for `Algebra.Bundles.Raw.RawX` bundles, and via `Setoid` instances, for `Algebra.Bundles.X`?

[jamesmckinna]

This is another instance of the issues arising when adding 'derived forms' to a(n algebraic) structure/bundle, namely where should they be added:

• to the RawX bundle? this is currently the case for _≉_, but AFAICT, never used, except to hereditarily be re-exported to richer structures;
• to the IsX structure? this is not currently the case for _≉_ via an IsEquivalence field, but is for IsGroup._-_ cf. #2251 ;
• to the X bundle? this is also the case for _≉_ via the setoid manifest field (#2095 , #2162 ), when that is in fact a 'derived form' defined in the IsX structure... and by the opening of the underlying RawX bundle.

The first and third cases seem to me to represent a clear DRY violation, and probably arise from the accumulation of 'legacy' design decisions. But what, if any, should be our refactoring policy towards a revised design?

Context: I'm working on a branch/PR addressing #2273 and find myself wondering whether (Raw)SuccessorSet needs explicitly to declare a negated equality symbol, when it should be (available to be) brought into scope via the Setoid instance of IsSuccessorSet...

UPDATED I've tried to regularise my vocabulary to avoid speaking of 'instance's of record types in favour of referring to their (often also record-typed`) fields, also often manifest, ie. defined rather than declared.

[jamesmckinna]

In the absence of further discussion yet, note there are two possible scenarios:

• where the derived operation indeed is derivable from the Raw signature (these are the 'easy' examples being considered under #2251 / #2268 );
• where the operation is only definable under the assumptions that the IsX axiomatisation holds (for some reason, the first example that I can think of is the 'snake lemma' for Abelian categories... but presumably 'easier' naturally occurring examples arise for theories simpler than the essentially-algebraic fragment? Maybe not!?)

I'm not sure what the official (universal algebra) nomenclature is for each kind, but on the model of the theory of formal systems, I supposed the first should be called 'derivable', while the second 'admissible'?

In any case, this issue concerns derivable operations being defined 'too late' to be exported to any subsequently definable extension of the algebra. And that does seem to be a DRY problem... over and above the 'where should such things live?' question...

[JacquesCarette]

Finally catching up on really old stuff - my mailbox is quite full of saved email about items that I meant to comment on. Still have 30 or so from 2024 alone, never mind a whole bunch from 2023!

I do agree that the library is over-eager to define 'helper' conservative extensions that turn out to be seldom used. (I don't know what the official nomenclature is either, but 'derivable' and 'admissible' make a lot of sense.)

I'm a bit concerned about solving DRY problems by over-defining things just on the off chance they might be needed. (Especially here as negation is so so often a code smell in constructive mathematics.)

Personally I'd prefer some 'helper' module(s) [with a better name than Helper !] that define extensions in a standard way. I've migrate things towards that in agda-categories -- it has really helped reduce bloat. (Monoidal was criminally bloated, which had non-trivial downstream effects.)

[jamesmckinna]

@JacquesCarette thanks for returning to this! And I appreciate you separating out two parts to this:

• what notions should be added automatically?
• where should they be added?

But here the problem is that, independent of any answer to the first, the second is answered in weird/bad/DRY-violating ways. So from my point of view it's not a case of being "over-eager", except inasmuch as contributors have not been clear what to add where, so have ended up duplicating structure... and in the case of RawX bundles, they are a relatively recent addition, so a certain amount of knock-on refactoring might have been anticipated/expected, but has not (yet) happened.

As to the first, I'm a bit 'wider' than you as regards extending record APIs, here out of a consideration for consistency of notation, as well as relieving the user of the burden of ad hoc invention, esp. in the context of a 'standard' library (along the lines of 'batteries included': 'if you open this, then you'll get all of this extra, for free'), and I'm willing to take the space hit... I think "bloat" is too strong here!

So a resolution of this issue for me would happily resolve the first question in whatever form (we should reach agreement... either as an 'extension' module, or as 'batteries included', and if so, how much?), but first how we consider appropriate to resolve/standardise the second...

[jamesmckinna]

As for _≉_ itself, it's perhaps unfortunate to have it in the title of the issue, which partly reflects that the underlying Setoid structures of an Algebra structure/bundle are defined under Relation.Binary, and, moreover, are not defined relative to a Raw (equality) relation (single field records tend not to get defined in the library, except for instance inference, and the Unit type as a special case...?), so it seems as though there isn't an obvious place to add negated equality as an additional manifest field...

... but your point about it being a code smell is an interesting one. Barring eg it's 'general' properties wrt Respects mentioned in #2341 ...

... so a possible 'better' place to add it would/might be as a manifest field of DecidableEquality (where it surely wouldn't be a code smell?) but for the fact that we'd then have to add 'the negation of A' as a manifest field to Dec plus a renaming opening for such objects... but that seems too horrible to contemplate!?

[JacquesCarette]

Through the many many words, talking about many fascinating issues... I've lost the thread about what is the main issue at stake here?

[MatthewDaggitt]

My view is that really the correct solution is number 1. It should be in the Raw bundles. I think the missing part of the puzzle is that we don't have a RawSetoid bundle in which to put the negated equality operator...

[jamesmckinna]

Through the many many words, talking about many fascinating issues... I've lost the thread about what is the main issue at stake here?

Yup, that's my weakness... (too) "many many words" ;-)

TL;DR: there are 2 issues at stake:

• (general) where should admissible/derivable operations live, so that we correctly export them in sub-structures/bundles; in general, I believe that derivable operations should live in the Raw bundle (but IsGroup is an anomaly, so _//_, _\\_ and _-_ should be moved to the RawGroup bundle...)
• (particular) the derivable _≉_ is an anomaly, for the reasons that @MatthewDaggitt points out (because RawSetoid doesn't exist; another possible downstream PR? in which case where should it live: under Relation.Binary.Bundles.Raw which would be new, or under Algebra.Bundles.Raw)

In each case, the solution would (seem to) be a fiddly (and possibly, for the IsGroup case, breaking) PR moving things around/adding new things, so suggest tagging this as v3.0 when we might reconsider this and eg. #2252 #2255 #2268 (though this could be dealt with independently in v2.1 as a prototype of how to fix it in general...?)

[Taneb]

RawSetoid, if we want to add it, should live in Relation.Binary.Bundles.Raw, and it should probably have some friends in there with it

[jamesmckinna]

@Taneb yup, all the various ordering relations and their flipped- and negated- versions should be in Raw bundles for such things... so maybe a v2.1 version is possible/desirable?