Redundancy in ring-like structures

[Taneb]

Consider, from Algebra.Structures

record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-isSemigroup : IsSemigroup *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

+-isMonoid and *-isSemigroup both contain a field isEquivalence : IsEquivalence _≈_. There is nothing forcing these to be equal (which might matter if _≈_ is proof-relevant). Also, it makes it a pain to implement a ring-like structure "top-down" (writing out nested records explicitly).

[MatthewDaggitt]

Yup, it is a pain. I would go so far as to say that the whole hierarchy is pain. How bad is it to flatten it out?

The only real way I can see to fix this in a composable manner is to have separate records for each structure, one with the equivalence and one without it. However that would be so earth-shatteringly non-backwards compatible that I hesitate to even suggest it.

[JacquesCarette]

At the risk of sounding like a broken record: we need more than what I call extend as an operation on record declarations, we also need combine. extend in this case is essentially disjoint union, but the one that works in a lop-sided way because the right part can depend on the left. combine is then a form of pushout.

The whole point is that one needs to be able to declare that two sub-structures are known to be (and must be) definitionally equal.

Then, from a usability point of view, I further argue that while library developers want to declare their structures in a highly compositional manner, library users would much prefer a 'flat' version. These are semantically equivalent (it doesn't take HoTT to prove that!), but far from equivalent from an ergonomics perspective.

Making sure that this all really works was the work of my PhD students Yasmine and Musa (and some of it was started in conjunction with Russell O'Connor, who was a post-doc with me at the time).

But it would need support inside Agda to work. It's almost feasible, but there's a problem with the scope checker that's blocking.

[MatthewDaggitt]

At the risk of sounding like a broken record

Haha, don't worry about it. I learn something new every time :grin:

But it would need support inside Agda to work. It's almost feasible, but there's a problem with the scope checker that's blocking.

That's exciting to hear how close you and your students are! Does the issue with the scope checker have an issue number on the Agda tracker?

[JacquesCarette]

https://github.com/agda/agda/issues/3699. The 'close' is not getting closer as the students have graduated... and I currently don't have any good candidates to pick that back up.

[jamesmckinna]

Hmmm. This problem (specifically, in the Ring case; generically ... I think it's been underexplored (flame hat on)) does indeed seem like a broken record, and advocates for various solutions add their own records (sic) to the pile. Forgive me if I get on my own hobby horse about this. But I'm happy to be pointed to more recent work! And yes, I am writing in (full) ignorance of the design principles for the library, so instructions to go away and educate myself might also be in order. Burstall and Lampson, in their (1984/1988) paper on "Pebble: A kernel language for abstract datatypes and modules" gave one account of extending modules that Luo dubbed "Pebble-style sharing" or "sharing by parameterisation" (to distinguish it from ML-module-style sharing; 'sharing by sharing' as it were); the distinction is essentially that between considering an algebraic structure as (a collection of) values/functions/properties/proofs applied to the underlying 'carrier' object (cf. type classes in haskell or Coq), and materialising that object as a dependent record/Sigma type which collects all the structure together. It's been a long-standing bugbear that such materialised structures are hard to extend; so much so that Spitters and van der Weegen in their development of an algebraic hierarchy on Coq, remodelling the earlier C-Corn library for the Fundamental Theorem of Algebra, took the Pebble-style route, even going as far as isolating classes containing individual operations, and taking advantage of type-class inference in Coq to, as I understand it, essentially do the materialisation on-the-fly (I'm more than happy to have their work re-explained to me if I've got the details wrong). Here, the discussion seems, once again, to be about Ring considered as a 'sharing-by-sharing' structure, and then the (usual) problem of ensuring that the shared common substructure be made suitably 'equal'/compatible (here, the underlying setoid of the carrier), in spite of the fact the extended (additive group; multiplicative monoid) structure seems to be implemented 'Pebble-style'. Can the problem be solved by exposing the underlying carrier setoids as further (explicit) parameterisation on which each of the other structures depends?

[jamesmckinna]

But I think that there is a different solution, for Ring at least, also under-researched, but which I see recur from time to time, as is, i think, a consequence of taking the universal algebra/set-based view of signatures and structures. Namely, instead to view 'Ring's as Monoid objects in the category of Abelian groups. One way to make this slightly less categorical, and not make a library dependent (sic) on underlying categories as the bases for algebraic structure, is to formalise the notion of 'monoid action on an Abelian group', as a vanilla algebraic structure built out of two independent components, a Monoid on blah, and an Abelian group on blah'... and then a Ring is nothing more or less than an Abelian which has a Monoid action on itself (thus identifying blah and blah' as a shared substructure ... and Pebble-style sharing seems easier here as the way to achieve this? cf. Spitters/vdWeegen). There are other structures where this kind of thinking (Bourbachiste?) helps, I think: towards matrix algebra etc. don't consider algebras first, but modules/vector spaces over rings/fields of coefficients, and only then define an algebra as a module/vector space over itself as coefficients etc. The 'trick', such as it is, seems (to me, at least) to lie in separating out independent structure in the general case, and then only identifying the 'special' instances by explicit identification of shared substructure. Library users might still want their preferred structures to be fully materialised as records, but that doesn't mean they have to be defined that way. I realise this may be a somewhat Quixotic mission to find myself on (it certainly is when I try to have discussion along these lines about class definitions in haskell), but it might be that I find a more sympathetic hearing in this community. That said, apologies for what might be breaches either of github, or agda std-lib, commentary etiquette; but it strikes me that people have been tying themselves in knots over Ring since as long as I have been a researcher in type theory, and ... here we are again?!

[JacquesCarette]

You might surprised by this @jamesmckinna but I pretty much agree. Yes, I am pushing 'my' solution, but

1. it's been directly and indirectly influenced by Burstall's work quite a bit, and
2. my solution has been optimized for a particular set of requirements, which might not be equal to those of agda-stdlib [In other words, my solution could be wrong for Agda. I'm still extremely interested in solving the problem.]

Spitters and van der Weegen needed to optimize their solution to fit within Coq's existing ecosystem, which is wildly different from Agda's. Furthermore, facilities in Coq have evolved quite a bit since, so it would be interesting to redo the work and see if there are even better solutions.

Probably the best 'guide' to a good solution lies in Arend. It blurs, automatically, the difference between parameters and fields. This makes sharing incredibly easier to deal with. The problem with current Agda (and Coq and ...) is that once you make a choice of encoding, then you are stuck with that choice. And the main observation is that there is no universal choice that is always ergonomic.

Note that for Ring itself, it is indeed possible to go the action route, and get something that's better. Unfortunately, that's a local fix which doesn't scale. We did slightly more than a 1000 theories in MathScheme, and we really needed a much more flexible notion of sharing. For one, a notion of sharing that does not involve renaming in its definition is doomed. Almost all current systems have this quixotic notion of "same name, same concept", which is fundamentally broken. Once you encompass more math than the usual undergrad curriculum covered in CS and get to things like Squag, Near semi field, Near semi ring, Diod, Moufang loop, Shelf, Rack, Spindle and Quandle (look them up, they're jolly good fun!), simpler solutions fall apart.

The solution, IMHO, requires seeing parametrized records and telescopes as "the same thing". The next leap is to not toss out the DAG structure inherent in telescopes, but to keep it firmly in mind. Then, as Arend does, you can freely move a 'cut' marker in and out, to indicate parameters vs fields. The parameters then indicate sharing.

This idea is buried in A language feature to unbundle data at will, and somewhat more explicit in Musa Al-hassy's PhD. Unfortunately Musa left for industry, so Wolfram and I will need to turn parts of it into paper(s); but because both of us have very heavy admin duties, we're putting it off until next year, when both will be on research leave (and my plan is to spend 1/2 of it in Scotland).

Thanks for the pointer to the Pebble paper. I had, sadly, not encountered that particular paper. It is indeed quite good.

[MatthewDaggitt]

@jamesmckinna thanks for your input, it's a very interesting read! I do agree with you that parameterising everything explicitly be a Setoid would probably improve things. However...

The story from my perspective is that the definition of Ring and others were already in the library when I took over, and since then various people have extended the hierarchy with other structures. We've tried to remove some of the more obvious wrong decisions, but I think most people acknowledge that it's being done the wrong way. There's been lots of different suggestions about parameter/field juggling from various people that aim to either improve or fix the situation. The reasons why nothing has been done is as follows:

1. Unless well-researched with the features and limitations of Agda in mind, it's not immediately obvious from the start what the drawbacks of a particular change are. Any large scale rewrite is going to be incredibly disruptive to a large part of the Agda community, so we really really want to be sure we're getting it right rather than merely improving the situation before we start anything.

2. In my non-expert opinion, I would agree with @JacquesCarette that there probably isn't a "best" way of formalising things and that any change is likely to introduce new problems at the same time as it fixes the existing ones. That to solve the problem once and for all we do indeed need a method of dynamically switching between parameters and fields.

3. Even if there is a "best" way, it would be an enormous amount of work even just to change everything within the standard library, as there are no refactoring tools for Agda. Finding someone to do the two weeks work is not easy.

[jamesmckinna]

Thanks to both @JacquesCarette and @MatthewDaggitt for the very constructive responses to what my have been my 'first thought, worst thought' (sic) wading in to the discussion, and for the pointers to additional reading, as well as a break down of the some of the high-level pragmatic issues facing the/any library designer(s). Apologies for being naive enough to insist on one solution to this particular problem, without considering the general case carefully enough first. And yes, hoisting out a deeply embedded design decision (eg the underlying setoid structure) for subsequent refactoring is not for the faint-hearted, and yes, there's definitely a non-trivial cost/benefit analysis to be done there before making any rash decisions (or promises).

But I'm definitely interested in the problems of extensible records (and other module-like structures), in this setting and elsewhere, so I'll... sit on my hands and think for a while. My thanks as well to @JacquesCarette for the extensive pointers, including to both MathScheme and Arend, neither of which I had come across before. Much food for thought!

[jamesmckinna]

And great to hear @JacquesCarette that you're planning to spend time in Scotland next year! Fingers crossed etc.