[DRY] defining concrete instances of `RawX` bundles

[jamesmckinna]

This is an offshoot of thinking about both #2252 and #1688 / #2254 (and perhaps requires precise resolution of the latter): why, in eg. Data.Nat.Base, do we write

-- Raw bundles

+-rawMagma : RawMagma 0ℓ 0ℓ
+-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  }

+-0-rawMonoid : RawMonoid 0ℓ 0ℓ
+-0-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  ; ε   = 0
  }

*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  }

*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
*-1-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  ; ε = 1
  }

+-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
+-*-rawNearSemiring = record
  { Carrier = _
  ; _≈_ = _≡_
  ; _+_ = _+_
  ; _*_ = _*_
  ; 0# = 0
  }

+-*-rawSemiring : RawSemiring 0ℓ 0ℓ
+-*-rawSemiring = record
  { Carrier = _
  ; _≈_ = _≡_
  ; _+_ = _+_
  ; _*_ = _*_
  ; 0# = 0
  ; 1# = 1
  }

when it might be simpler/better/DRY to write instead:

+-*-rawSemiring : RawSemiring 0ℓ 0ℓ
+-*-rawSemiring = record
  { Carrier = _
  ; _≈_ = _≡_
  ; _+_ = _+_
  ; _*_ = _*_
  ; 0# = 0
  ; 1# = 1
  }

open RawSemiring +-*-rawSemiring public
  using ()
  renaming ( +-rawMagma to +-rawMagma
           ; *-rawMagma to *-rawMagma
           ; +-rawMonoid to +-0-rawMonoid
           ; *-rawMonoid to *-1-rawMonoid
           ; rawNearSemiring to +-*-rawNearSemiring
           )

Also (incidental historical glitch?): why do the first four bundles not need to specify the Carrier, while the last two do? Or are they all, in fact, redundant?

UPDATED (following @MatthewDaggitt 's and @JacquesCarette 's comments below):

+-*-rawSemiring : RawSemiring 0ℓ 0ℓ
+-*-rawSemiring = record
  { _≈_ = _≡_
  ; _+_ = _+_
  ; _*_ = _*_
  ; 0# = 0
  ; 1# = 1
  }

open RawSemiring +-*-rawSemiring public
  using (+-rawMagma; *-rawMagma)
  renaming ( +-rawMonoid to +-0-rawMonoid
           ; *-rawMonoid to *-1-rawMonoid
           ; rawNearSemiring to +-*-rawNearSemiring
           )

[MatthewDaggitt]

Hmm this is mainly a legacy of not wanting to structure the non-Raw bundles like this. There's no particular reason why they couldn't be structured like this.

Also (incidental historical glitch?): why do the first four bundles not need to specify the Carrier, while the last two do? Or are they all, in fact, redundant?

They are all redundant.

[JacquesCarette]

I would sure welcome such a rewrite. We should "use the structure of the math" more.

And I guess the first 2 renames are not needed at all?

[jamesmckinna]

@JacquesCarette , you wrote:

And I guess the first 2 renames are not needed at all?

See the (revised) deployment of the proposed pattern in https://github.com/jamesmckinna/agda-stdlib/blob/modular-arithmetic/src/Data/Integer/Modulo.agda

Refactoring Data.Nat.* to reflect the pattern can perhaps/probably wait for a 'free' moment... later ;-)

[JacquesCarette]

Can you please write out the pattern? I don't know what parts of that file is "the pattern" and what is just code.

[jamesmckinna]

OK, but as a placeholder for now, what I envisage as "the pattern" is to replace a succession of individual RawX definitions with a single one, for the 'richest' such structure/bundle, on the assumption that the corresponding Structures/{Raw}Bundles definitions support bringing all the substructures into scope with a single open... ... but indeed I'll try to be more explicit as to how I'm doing that in the ~~PR~~ code that I claim exhibits it... viz. in these lines: https://github.com/jamesmckinna/agda-stdlib/blob/edfe8173b48fad2db556922469d9802b4320d9d1/src/Data/Integer/Modulo.agda#L73-L92

[jamesmckinna]

(Some while ago... @MatthewDaggitt wrote)

Hmm this is mainly a legacy of not wanting to structure the non-Raw bundles like this. There's no particular reason why they couldn't be structured like this.

Revisiting this in the light of my just-posted #2391 , and having dealt with the complexities of the re-export strategies in Algebra.Structures and Algebra.Bundles under #2383 , I wonder if this is really the case now? I know that the record structures are basically 'flat', but the hierarchy now does a huge amount of rebuilding, and importantly for this issue, public re-exporting of such sub-structures/sub-bundles...

[jamesmckinna]

Re: documenting "the pattern" @JacquesCarette I realise that it's a bit hard to say more than "create the 'largest'/'richest' structure/bundle available, and then open it publicly to bring all the sub-structures/-bundles into scope, renaming if necessary"... I guess that's why I called it a 'pattern'... but see also #2391 for more exemplars of it?