[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.

[jamesmckinna]

Notes to self (and the future): currently, Algebra.Bundles.Raw correspond to single-sorted, first-order, universal (if that's the right terminology) algebraic signatures (bundled with their Carrier)

What happens if we try to add (structures and bundles for) essentially algebraic signatures?

Suggest introduce Algebra.Signatures and deprecate Algebra.Bundles.Raw, and index structures by the underlying signature, as in this issue.

Suggest signatures be parametrised by their Carrier (Pebble-style), so that we're not precisely emulating their 'bundled' versions as in Raw?

[JacquesCarette]

One argument against punting this [...]

Amusingly, I find this all too abstract to figure out whether I agree with you or not. Could you give a very concrete example of each issue? Pick your favourite structures and derived operation to illustrate what you mean?

I do agree that the second inconsistency does seem to be something we ought to fix.

Suggest introduce Algebra.Signatures and deprecate Algebra.Bundles.Raw ... signatures be parametrised by their Carrier

Agree on both points.

[jamesmckinna]

One argument against punting this [...]

Amusingly, I find this all too abstract to figure out whether I agree with you or not. Could you give a very concrete example of each issue? Pick your favourite structures and derived operation to illustrate what you mean?

The current standing examples of RawGroup and IsGroup are what I have in mind here... but will try to work this up into a more detailed analysis...

[jamesmckinna]

To try to put my finger on it more precisely: #2251 is forced to establish the IsQuasigroup and IsLoop properties of a given (Is)Group under Algebra.Properties.Group rather than as manifest fields of Algebra.Structures.IsGroup for (at least) two reasons:

• (silly) Algebra.Structures defines IsQuasigroup and IsLoop after IsGroup because of its taxonomy based on number and arity of operations in the signature;
• (serious) the underlying RawGroup doesn't have access to the derivable _//_ and _\\_ operations, so we can't even talk about them as having IsQuasigroup or IsLoop properties without first defining them as part of IsGroup; this is possible, but conceptually undesirable, because their definitions don't depend on any properties of being IsGroup, only the signature of the RawGroup operations

Now, I suppose it is (perhaps) a moot point whether we regard IsQuasigroup and IsLoop as 'intrinsic' properties of any IsGroup structure, ie definable as manifest fields of Algebra.Structures.IsGroup by analogy with all the other structure-erasing 'inheritance-derived' fields of other algebras, or whether they are 'extrinsic' properties, definable in Algebra.Properties.Group, but it seems that this relies too much on some contingent identification of operations _//_/_\\_ which happen to obey the axioms, rather than the actually canonically definable ones, which are moreover definable in terms of the underlying RawGroup signature, and don't even rely on the IsGroup properties (although obviously the proofs of their IsQuasigroup and IsLoop properties do so rely). But the way we have things structured (and parametrised) at present seems to militate even against being able to make the choice... which seems A Bad Thing?

[jamesmckinna]

Also: extensibility An IsX structure parametrised over a fixed signature (such as we have it now) isn't susceptible to being given a RawY parameter which potentially extends that of (the implied) RawX... whereas record (telescope) subtyping would permit that...

[jamesmckinna]

Rebadged as a [DRY] issue