Redundant `zero` field in `Algebra.Structures.Biased.IsRing*`? about agda-stdlib HOT 7 CLOSED

I honestly don't know what the point of IsRing* is. Distressingly I didn't write anything about it or include it in the CHANGELOG. So yes, I guess it could just be deprecated...

from agda-stdlib.

Absent any reaction to this, I did some digging into the history of Algebra.Structures.Biased:

• commit 3c12349 introduced IsRingWithoutAnnihilatingZero, now deprecated by #2209
• commit 1de3223 four years later, introduces additionally IsRing*, with now-redundant field zero, but has otherwise identical fields to IsRingWithoutAnnihilatingZero, but is not (yet) deprecated...

Suggest that we make the breaking change to remove the declared zero field from IsRing*, but retain it as a 'biased' smart constructor for IsRing, as now. But given that IsRingWithoutAnnihilatingZero would then be identical toIsRing*, it seems as though it would further make sense to remove the construction of the manifest zero fields of IsRingWithoutAnnihilatingZero in favour of opening the IsRing instance (which now does define zero as a manifest field...) given by the IsRing* data...

... PR eventually incoming?

from agda-stdlib.

My understanding is that the reason for all this back-and-forth is that the hierarchy was too coarse initially, and so things that ought to have been true weren't because there were 'jumps'. Once you start being more fine-grained, you can have your 'inheritance' go via the "correct" theories. [At least, that's what happened when I was doing the same thing in MathScheme.]

In other words: the 'obvious' relation that arises amongst known theories "higher up" in the chain arises from relations from entirely unnamed theories lower down! "Pointed commutative Magmas" anyone?

I'm not aware of other redundancies, but there certainly could be more.

from agda-stdlib.

@JacquesCarette you make interesting, important points, and I'm sorry if the vagueness of this issue failed to home in on the much smaller, constrained, points I'd been trying to make (maybe writing issues needs a style guide !? ;-)) as an extended meditation on DRY-related issue arising from #2195 / #2209 :

• IsRingWithoutAnnihilatingZero is now deprecated, while IsRing* is not;
• IsRing with its zero field is 'obviously' redundant/deserving deprecation, in the way that both #2195 and the original introduction of IsRingWithoutAnnihilatingZero make/made clear; (shoutout to @Taneb as to whether you agree with this analysis?)
• IsRing* without its zero field is identical to IsRingWithoutAnnihilatingZero, and/but arguably, still worth retaining (rather than deprecating) as a 'natural' biased version (and name for it) of how to present an IsRing instance;
• each structure (implicitly) reduplicates the definitions of zero now associated with the unbiased IsRing, yet neither defines its own zero fields by simply opening its own manifest IsRing field publicly, and exporting those definitions...

So, my proposal was to:

• make the breaking change to IsRing* of removing its zero field (I've seen no stdlib client use this structure, but I think the same ambient justification for the breaking #2209 could be mobilised here);
• if necessary, explicitly export its zero field by opening its manifest derived IsRing instance;
• change the deprecated definition of IsRingWithoutAnnihilatingZero to basically be an alias for IsRing*, rather than recapitulate the definitions of zero already given in Algebra.Structures.IsRing(WithoutOne)

But, as I started to think about this (and my thinking has clearly evolved on this), it occurred to me that there might be other redundancies/ possible deprecations, arising entirely from #2195, rather than embracing any other nodes in the Algebra hierarchy, to do with the various substructures of IsRing. But @MatthewDaggitt 's comments on #2209 suggest (rightly, I think) that such things should be left to a subsequent refactoring of eg IsNearring ... #2212

One reason this is on my conscience is that I was the reviewer for #2209, and didn't take the time or care to (re)think all of the above at the time... which if I had might have made it a better contribution. Hope this clarifies!

from agda-stdlib.

An alternative proposal would, of course be simply to likewise deprecate the current IsRing*...

from agda-stdlib.

Incoming... #2357

from agda-stdlib.

Suggest we now close, given #2357 has now been merged.

from agda-stdlib.