Comments (7)
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 fieldzero
, but has otherwise identical fields toIsRingWithoutAnnihilatingZero
, 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 open
ing 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, whileIsRing*
is not;IsRing
with itszero
field is 'obviously' redundant/deserving deprecation, in the way that both #2195 and the original introduction ofIsRingWithoutAnnihilatingZero
make/made clear; (shoutout to @Taneb as to whether you agree with this analysis?)IsRing*
without itszero
field is identical toIsRingWithoutAnnihilatingZero
, and/but arguably, still worth retaining (rather than deprecating) as a 'natural' biased version (and name for it) of how to present anIsRing
instance;- each structure (implicitly) reduplicates the definitions of
zero
now associated with the unbiasedIsRing
, yet neither defines its ownzero
fields by simplyopen
ing its own manifestIsRing
field publicly, and exporting those definitions...
So, my proposal was to:
- make the
breaking
change toIsRing*
of removing itszero
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 derivedIsRing
instance; - change the deprecated definition of
IsRingWithoutAnnihilatingZero
to basically be an alias forIsRing*
, rather than recapitulate the definitions ofzero
already given inAlgebra.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.
Related Issues (20)
- Add bundles for lattice-like and module-like morphisms
- Document `variable` block indentation style HOT 5
- [DRY] what's the best way to `public`ly re-export properties/structure? HOT 5
- Use the Monoid structure of Endomorphisms to define powering HOT 1
- [DRY] More redundant `zero` fields in `Algebra.Structures`
- Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole HOT 5
- What's the 'right' notion of equality between functions? HOT 7
- [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)
- Rename `WeaklyDecidable`? HOT 4
- Add `Algebra.Properties.IdempotentCommutativeMonoid`
- Naming of new functions `tail∘inits` and `tail∘tails` HOT 5
- comments on lib-2.1 candidate 1 HOT 9
- Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer HOT 7
- Style for lower/upper case for initial letter in denotations HOT 7
- Restore missing proofs from `Algebra.Operations.CommutativeMonoid`
- Proofs in `Data.Vec.Properties` take general properties as inputs HOT 23
- Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365 HOT 3
- [DRY] Refactor the various definitions of 'pointwise' equality on functions/`Function`s/pointwise `Algebra`s HOT 2
- Data.Nat.Properties.≤-total should be implemented with _<ᵇ_ HOT 14
- Data.List.upTo/applyUpTo can be made faster HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-stdlib.