[DRY] Reconciling the indices of `IsX` with those of the corresponding `RawX`

[jamesmckinna]

Looking again at README.Design.Hierarchies, Algebra.{Module.}Structures and Algebra.{Module.}Bundles.Raw, I can't help wondering at the mismatch in indices vs. fieldnames to the various IsXs, with the correspondingRawX (although this may simply be an artefact of parametrisation of the Algebra.Structures module), but my main question is:

• why are the IsX records not indexed over a single underlying RawX parameter? (this may be historical...)
• should they be? (ie. should we at least reconsider revisiting this design...) (UPDATED: see below)

Apologies if my ignorance of the history of, and discussion on, the associated issues/PRs obscures what otherwise may be glaringly obvious to those more expert than me!

E.g., to define IsMagmaR in this style, and show it gives rise to a 'usual' IsMagma (and Magma! because the existing hierarchy permits this... so a genuine replacement, rather than enhancement, of the existing hierarchy would still require IsX and X to be separated; but here the existing concrete Raw bundles in eg Data.Nat could be generated using this extension instead...) instance etc.:

open import Algebra.Bundles
open import Algebra.Bundles.Raw
import Algebra.Definitions as Definitions
import Algebra.Structures as Structures
open import Level using (Level; _⊔_)
open import Relation.Binary.Structures using (IsEquivalence)

module Algebra.Structures.RawIndexed where

private
  variable
    c ℓ : Level

record IsMagmaR (raw : RawMagma c ℓ) : Set (c ⊔ ℓ) where
  open RawMagma raw
  open Definitions _≈_
  field
    isEquivalence : IsEquivalence _≈_
    ∙-cong        : Congruent₂ _∙_

  isMagma : Structures.IsMagma _≈_ _∙_
  isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Is it because to define any instance of a hypothetical IsMagmaR rawMagma one first has to (already have) open RawMagma rawMagma to be able to define the fields? Is this such a high price to pay?

The above may be a con, but pro might be not having to redefine in RawX the manifest operation fields defined in IsX... cf. #2251

Moreover, redefining the bundle X takes on the satisfyingly generic X = Σ RawX IsX form:

open import Algebra.Bundles.Raw
open import Algebra.Structures.RawIndexed
open import Level using (Level; suc; _⊔_)

module Algebra.Bundles.RawIndexed where

private
  variable
    c ℓ : Level

record MagmaR c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    rawMagma : RawMagma c ℓ
    isMagmaR : IsMagmaR rawMagma

[JacquesCarette]

This is yet another form of the eternal bundled / unbundled question. The correct answer is: don't choose, they are equivalent. Pragmatically, that remains a non-answer because, in Agda, this equivalence can only be witnessed tediously on a case-by-case basis.

Unfortunately, I have no idea what the actual ergonomics of each choice is. This would need a great big (costly) experiment, and it doesn't seem to me that we can decide this just as a thought experiment.

In theory, I personally like to group things together more. But that's at the "gut feel" level rather than at the "let's make this the design NOW" level.

[jamesmckinna]

Well put, and so I guess I defer to your wise insight. Sigh... That said, if there were an agency willing to fund the costly experiment, ... or indeed, whether your remark is enough to encourage a zealot to pursue it for its own sake anyway... ;-) (best not, but the devil on my shoulder, etc.)

And... I don't think I was proposing it as THE design, but as with Algebra.*.Biased, as an alternative means to an end...

[MatthewDaggitt]

I've also wondered about this from time to time, and I think it's mainly a swings and roundabouts issues. As you say, one of advantages is that you can import Structures while fixing the equality. This a feature that we use relatively widely in the library.

I agree with @JacquesCarette's points as well that this may be a language design question.

If no one objects, then I might add this to the hypothetical-rewrite milestone.

[JacquesCarette]

Well look at that, a hypothetical-rewrite milestone - very nice.

Hmm, I'd be tempted to start a page on the Wiki also collecting language changes that we library writers would really like to see.

[jamesmckinna]

One argument against punting this to the indefinite future with hypothetical-rewrite: the issue(s) arising from #2251 and #2268 : if we add derived operations to the Raw bundle (which makes sense from the point of view of them being 'raw' operations), then they don't get inherited in the IsStructure definition, only in the Bundled version. But if we index the Structure.IsX on the RawX bundle, then we get them 'for free'.
Similarly (a related, but distinct, issue): Algebra.Properties.X expects a Bundled X, instead of (more simply?) an instance of IsX... is this the 'correct' factorisation of the dependencies?

And the second: consistency/uniformity. We index homomorphisms between Structures.IsX and Bundles.X via their underlying RawX bundles, so 'on morphisms' we observe one discipline, but 'on objects' another... which seems an anomaly worth correcting.