Indexing and parameters for Algebra (and the like)

[JacquesCarette]

@jamesmckinna draws our attention to #2252 and other choices of bundling. Using our new vocabulary, the discussion amounts to:

1. Whether IsX should be indexed by a "bundled up" signature rather than an exploded one. The exploded version gets really tiresome once there are many pieces of data in the signature. The counter is transport hell when "bundling up" hides details.
2. Whether we should embrace the MonoidOn style. This would mean that IsMonoidOn would actually, given the style above, have two parameters: the carrier and the bundle of function symbols. One could then have a MonoidOn that that shifts the bundle of function symbols into fields (and the axioms as a single field, as now) while keeping the carrier exposed.

Previous discussions also touched on the issue of conservative extensions, i.e. admissible definitions that are available as soon as one has the right vocabulary in hand. But such conservative extensions have different forces acting on the design, and should be discussed elsewhere.

[jamesmckinna]

I'm unfamiliar with MonoidOn style... a pointer would help so that I can get up to speed.
UPDATED: Just read Vocabulary, so I'm good now. Hate the terminology, but have got the idea.

[jamesmckinna]

Re: 1

I'm in favour of 'bundling up', viz. making RawX the base for all (structure) parametrisation ('all' perhaps to be taken with a pinch of salt given other comments form @JacquesCarette ), subject to the following provisos:

• the underlying Carrier/A should be a 'Pebble-style shared' parameter (implicit) to the bundle consisting of ...
• the 'equality' relation plus the operations; that is, I only really want to interpret the X-vocabulary relative to a specified equality
• that structure IsX should index on such a RawX (this is the substance of [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252)

NB under the first proviso, the Raw hierarchy would no longer as such be (meta-level) below Algebra.Bundles, as these would still actually bundle the Carrier as well... but probably there are still things to iron out about my position...

Pro:

• avoids explosion as noted
• makes a clear delineation so that subX/X/quotientX can all be defined relative to a given Carrier (never usually needing mention), because the equality can be varied (or not!), along with the 'signature' specification, in a single gadget
• because I personally pragmatically want 'definitional'/conservative extensions of the ostensible signature to be available as manifest fields of (a 'wide' version of) the given RawX, and available when defining structures/bundles on top of it merely by opening (if necessary the 'wide' construction applied to the RawX thing). My standing example of RawGroup admitting RawQuasigroup and RawLoop subsignatures (and their corresponding IsX/IsY/IsZ substructures) being a case in point Add new operations (cf. RawQuasigroup) to IsGroup #2251
• because the current RawRelation, better perhaps RawSetoid, is then a (degenerate/limiting) case with empty signature, with [DRY] why is _≉_ defined both for Algebra.Bundles.Raw.RawX bundles, and via Setoid instances, for Algebra.Bundles.X? #2274 then tackled as merely another conservative extension of RawSetoid, and hence available through the hierarchy from the ground up.
• ... to be continued ... (?)

Con:

• any arising from 2./IsMonoidOn I'll tackle separately, but I'm alive to a current stdlib design decision to define (sub)structures by projection (IsMonoid a projection from IsGroup, rather than RawGroup is RawMonoid plus _⁻¹, but that can be achieved by existing record subtyping in Agda...?)
• we lose the ability to share parametrisation wrt equality in Algebra.Structures, but that may not be so much of a deal-breaker if in any case we begin to experiment with breaking up such monolithic modules
• what do we do about 'bare' structures based on operations-without-equality (eg @laMudri 's setoid-from-bare-preorder Orders without equivalence relations #2070 via Relation.Binary.Construct.Interior.Symmetric [ new ] symmetric core of a binary relation #2071 ) although I think they could be handled similarly to that example?
• ... to be continued ... (?)

[JacquesCarette]

I should explicitly note that I despise the RawX name. These are signatures. I would absolutely be fine with having Algebra.Signatures be part of the namespace. I don't when/why RawX originated -- but yuck!

We also have to be careful about the relations between signatures/theories and the relations between their models (instances), as the variance changes.

It looks like we have a 4-level bundling problem: 1) carrier(s), 2) equality(ies), 3) function + relation symbols, 4) axioms/properties. Well, even more levels if you count definitional extensions. And I'm guessing that I don't even have the true complexity mapped out properly.

If I understand @jamesmckinna 's proposal above, I definitely am sympathetic towards it. But I don't want to "solve it in the small" only to have it bite us really hard "in the large" later.

[jamesmckinna]

[moved from #3052]
Regarding Algebra.Signature, for sure I have no particular attachment, other than acquired-familiarity (the bane of legacy knowledge), to Raw, and in a post which draws attention to making namespaces work harder, I surely could have thought harder about what name we might want for this important semantic notion! But prior to stdlib, I'd never explicitly seen the structure/bundle distinction made, or so named as such. Post-Pebble, the ideas were clear, and frequently discussed eg by Luo in various papers on algebraic specification and his book, but it took me a while to internalise what I took to be Agda-local/stdlib-local vocabulary. So, having also internalised Raw... that's what I used.

That said, given that this is a discussion about design (and thus, perhaps more targeted towards a hypothetical-rewrite made flesh...) I'd be happy to stick with existing stdlib names for the sake of incrmenetal progress now, with a more comprehensive overhaul later. A rare instance of how working on stdlib is making my thinking more bottom-up rather than my default top-down!

[jamesmckinna]

I tried to find out when raw first appeared, but surprisingly, git blame couldn't help, so I resorted to the brute-force grep 'Raw' CHANGELOG/*.md:

• Raw bundles seem to appear in v0.17
• concrete instances in eg Data.Nat.Properties in v1.2

UPDATED Nope, we're in Original Sin/Before Times territory:

• the original port to GitHub in 2009 from the darcs repo already appears to contain in Algebra.agda: of all things RawMonoid!!!

[JacquesCarette]

Ah, I did not get a notification of the update. I also found out that indeed, this goes back to the 'before times'.

[jamesmckinna]

Re: 2.
I realise that Once Upon A Time there was discussion/lore about IsXOn, but I struggle to either find it, or digest it, or work out how particular conclusions were reached as to the Right Way to do things (there may not be one, only Choices with Consequences/Tradeoffs).

I think we don't need IsXOn, unless we see it as a convenience step to packaging a given IsX rawX (for [ rawX : RawX {A} ] for a re-fashioned/refactored Algebra.Structures.IsX, even under my suggestion/proposal above that we index on RawX which contains equality built-in as a field.

Firstly, even to state 'equational' axioms, we need equality in scope... an operation _∙_ : Op₂ A is only ever going to make sense as a monoid/semigroup operation relative to such an equality (IsMagma is so low level that it's hard to want to make a special case for it, and in any case, we demand a ∙-cong field as well), so it feels 'natural' to see any axiomatisation as relative to operation+equality.

Secondly, how often, really, do we consider definitional situations of the form ' IsX rawX consists of an isY : IsY rawY together with an isZ : IsZ rawZ, plus some more axioms, where rawX : rawX etc. are not already definable/defined as part of the definitional extension of RawX by manifest fields exhibiting appropriate subsignatures? Now, we don't currently do this as such, because the RawX hierarchy is a relatively late element of the design... but in principle, our current approach to extending structureisX via projection with its substructures isY, isZ could be pushed down one level to rawX etc.? It came initially as a surprise to me that the stdlib design philosophy of 'projection' of substructure (despite all the boilerplate sometimes required) seems actually 'better' (for a suitable definition of 'better'!?) ergonomically than the old-style inheritance/superclass-via-instance approach initially championed in Agda...

... sidebar: I think this is the case specifically for the Algebra hierarchy, it may be that more general takes on 'algebraic' specification might want/expect/even need a more flexible library of 'theory combinators' for putting IsX things together than we have at present... so perhaps a call-out to experts such as Peter Mosses for this kind of thing? (Despite my heritage as school-of-Burstall... oh what a bad student I was!)

As for actually putting RawY and RawZ signatures together into RawZ,

• what is the semantics of rawX = record { rawY ; rawZ } in terms of record subtyping if rawY and rawZ both have a _≈_ field, even if they are/happen to be definitionally equal?
• and why doesn't Agda support such combination of record types at the type level? (maybe this is the CAS/algebraic specification question/problem?)

I'm pretty OK with writing rawGroup : RawGroup = record { rawMonoid ; _⁻¹ = ... } for individual constructions, but vaguely peeved, and perhaps should be more definitely so, that I can't apparently write

record RawGroup where 
  RawMonoid
  field _⁻¹ : Op₁ A

except that... maybe this is yet another instance of 'use composition, not inheritance', and the correct thing to do is indeed what we do now, namely

record RawGroup where 
  field rawMonoid : RawMonoid
  field _⁻¹ : Op₁ A

and manage superclass inheritance via explicit projection rawMonoid.

All that said (and yes: Ring/Semiring seems always to come up in 'coproduct of theories' vs 'tensor product of theories' discussions as examples of 'a Ring is an IsY and an IsZ subject to a distributive law' seemingly requiring an IsYOn and IsZOn analysis of the substructures, but I've always argued that this is the Wrong Way to think about Ring: it's an AbelianGroup with a (multiplicative!) MonoidAction of its carrier on itself, otherwise a Module over itself... yet another sidebar, plus a call to have not just Algebra but also Algebra.Action... #2348 / #2350)...

... what are the arguments in favour of IsXOn? And how do they stand up, given that we don't actually employ such a design currently...?

[JacquesCarette]

The name of the problem (under the question of "what is the semantics of rawX = record { rawY ; rawZ } in terms of record subtyping if rawY and rawZ both have a _≈_ field, even if they are/happen to be definitionally equal?") is "the diamond problem". Whereas the same problem for implementations is awful, the problem for theory declarations is quite tractable. In the 'right' categories, it amounts to pullback along display maps. Of course on 'raw telescopes', things are not as nice. But bottom line is: you never want to rely on coincidences, like the system being able to work out definitional equality. That is extremely fragile.

IMHO, the reason Agda doesn't support such combinations of record types is that type declarations are not first class. Plus it is unclear if that operation makes sense for 'record types'. It certainly does for signatures and theories -- but record types are merely an almost-adequate representation of the core information contained in a theory presentation.

The IsXOn way of things actually is present in mathematics too: R-module and R-S-bimodule are prominent examples. It's just that the On version is the simple version. In that version, you simply want the system to have the a priori knowledge that various 'structures' (in the mathematical sense) share the same carrier(s), definitionally. Not by accident, but by forceful act of declaration of intent. If you try to work with (say) a Monoid and a separate AbelianMonoid structure on the same carrier, you'll see the subst hell you get into very very quickly; it is more than ergonomics failure. At the other opposite end, working with super long telescopes (our current IsX) gets quite tiresome too - but at least that is mere ergonomics failure.

[jamesmckinna]

Sorry to be ignorant/obtuse. I don't see how R-module and R-S-bimodule are IsXOn instances? I think of those, paradigmatically as with Ring, of AbelianGroup on the one hand, with RingAction by scalars on the other.

[jamesmckinna]

Separately, re: your Monoid/AbelianMonoid anti-example... collecting together a 'library' of HowNotToDoIt anti-examples would be independently useful? Then I could see the subst hell that you have already witnessed, without having to recreate it in my own home, as it were ;-)

Separately, though: "a Monoid and a separate AbelianMonoid structure on the same carrier"... Isn't this an argument in favour of

• Carrier is a Pebble parameter
• equality is separately part of each of the Monoid/AbelianMonoid structures involved?

Ie "a priori knowledge that various ... share the same carriers, definitionally" [my emphasis added] is the essence of Pebble-style sharing?

[JacquesCarette]

R-modules are a general form of the On pattern. If you view a theory as being equivalent to a telescope, then both 'cleave' the telescope in a particular spot, putting everything that's on the left as parameters, everything on the right as fields. Which is the implementation of what mathematicians mean by R-module: all the ring stuff is fixed (and you are parametric in it), and all the module stuff needs to be defined. The On pattern is just special case when you let the carrier poke out.

I may have picked a bad example for you as you think of these as being arranged differently as theory presentations, so my analogy indeed does not resonate in that view.

[jamesmckinna]

Re: diamonds. We promised ourselves that we would archive @laMudri 's discussion on #898 / #985 so that it didn't get lost in closed issues/merged PRs... For now, a link from here will have to do!

[JacquesCarette]

Yay for @jamesmckinna the archeologist!