Vocabulary (IsX, RawX, structures, bundles, etc)

[JacquesCarette]

[I chose 'General' because this is meta, about the vocabulary we use and the concepts behind it.]

Let me thus link some of the stdlib-specific terminology with broader concepts. Below X is always used as a meta-variable that stands for things like Monoid, Ring or Squag.

1. RawX: most others would simply call this a 'signature'. It is represented in Agda as a record. Under that reading, RawMonoid makes little sense, as without its laws, a Monoid is a PointedMagma. But a signature (i.e. something that defines carriers and function symbols, with relation symbols sometimes also being allowed) is an incredibly useful item, as it defines a local vocabulary that one can then use to define further concepts.
2. IsX: this is basically a predicate. Represented as a parametrized record, it is used to encapsulate a set of axioms (i.e. what upgrades a signature to a theory presentation). Its reading is basically "given the data of all the parameters, used as vocabulary, that data forms an X if one can witness all of the contents of this record". This is how the record acts as a predicate: it is contingent on being inhabited. IsMonoid does make sense on the exploded data of a PointedMagma.
3. structure: this is a name for IsX predicates.
4. bundle: this is a name for a record that has exactly the data that corresponds to an IsX predicate as fields, and then a single additional field for that IsX. Basically this is a "bundled up" version of a theory presentation, in the same way that IsX is maximally unbundled.

Formally, something like IsMonoid and Monoid are actually equivalent, in the sense that they have the same models. However, inside type theory, they are 'different'

1. they live at different universe levels
2. it is easy to have two "monoids" on the same carrier set when done via IsMonoid, but awkward using Monoid. The information flow is extremely different (it is foreknowledge in IsMonoid and post-facto for Monoid, and mixing things in the latter style ends up in transport hell.)

Much ink has been spilled about (un)bundling. Agda's choices are to support maximal unbundling (IsX) and maximal bundling (X). This is unsatisfactory, because carrier sets and operations are another gradation of signatures, and so that too wants degrees of bunding. For example, one will see MonoidOn in the wild, which is the bundle of everything except the carrier. In stdlib's case, MonoidOn might well want to have the carrier Setoid be what is exposed. Or both.

[jamesmckinna]

Re MonoidOn style (horrible terminology!).

My own position, untested against any hypothetical-rewrite, would be: (watch this space)

Sorry, just realised I should post this on #3053

[JacquesCarette]

I agree that it is bad terminology! I think it is the current least-bad that people have come up with. High praise, isn't it?

[jamesmckinna]

Re:

it is easy to have two "monoids" on the same carrier set when done via IsMonoid, but awkward using Monoid. The information flow is extremely different (it is foreknowledge in IsMonoid and post-facto for Monoid, and mixing things in the latter style ends up in transport hell.)

I feel the moral, as well as scientific/technical, obligation, to draw the distinction between

• 'Pebble-style' aka 'sharing by parametrisation' sharing (IsX structure style)
• 'SML-style' aka 'sharing by sharing' sharing (X bundle style/SML structure/functor style... ouch ;-))

as further (meta-level) vocabulary for talking about such things. SML avoids transport hell by... magic, and not having dependent types, so definitional equality between (shared) structures can be achieved by ... magic, timestamp/pointer equality under the hood... but I'm not sure what the current state-of-the-art is in eg OCaml...

NB SML-style is capable of supporting Pebble-style, by lifting each structure into a functor parametrised over the Pebble parameters, but for whatever reason, that idiom isn't often explicitly exposed in SML tutorials...

[JacquesCarette]

OCaml avoids this by similar magic. It's basically a sort of post-facto pullback based on accidental (but by-design accident) of names. Really extremely horrible. Pullbacks where one leg is a display map work just fine, but ought to be seen at the 'theory morphism' level rather than as signature operations.

'Sharing by parametrisation' makes a lot more sense. Arend makes that easy, as did Musa Al-hassy's work in his Ph.D. where he introduces the "waist" of a theory (which is the movable location in a theory presentation, seen as a telescope, that splits between parameters and fields).

[jamesmckinna]

I'm delighted that there are alternative frameworks in which it may be possible to Do The Right Thing, but this is a library for Agda we're talking about, so unless we can argue strongly to the developers for upstream changes, then these discussions aren't really going to go anywhere? (I know that at the moment, we are perhaps only re-codifying positions that have recurred in discussion on individual issues/PRs, so it's good to get them written down, but I'm also a bit frustrated by the gap between what might be achievable later, and what's achievable now. The old me would have held out for the revolutionary future. The new me, older now than the old me, wants what's achievable, moreover observably (?) better, today. How ironic!

[JacquesCarette]

I like understanding the 'correct' design as a prelude to figuring out the least-evil compromise given current constraints. If we are not willing to implement the upstream changes ourselves (which I'm quite sure in more cases we don't), then we do have to be willing to compromise to make progress today.

I probably should have spelled that out earlier!

[jamesmckinna]

A sidebar on meta-level vs. object-level vocabulary, as it (now; going forward; hypothetical-rewrite territory) cashes out in the hierarchical organisation of the library:

• maintaining as concrete names the surface tokens X, IsX, RawX, ... by virtue of their having clear (!?) semantic correlates, even if only at the (meta-)meta-level, seems to less like a cost worth paying...
• there are the 'historical'/'conventional mathematical'/'legacy' choice: eg to distinguish IsPartialOrder from Poset when we pass from structure to bundle... ditto. IsEquivalence and Setoid
• RawX, when added later, needed a 'new' namespace to occupy, moreover with individual names organised together in Algebra.Bundles.Raw, so that we now have the far-from-succinct names such as Algebra.Bundles.Raw.RawMonoid
• the issues I've raised before [DRY] defining concrete instances of RawX bundles #2255 [DRY] what's the best way to publicly re-export properties/structure? #2391 etc. which concern how best to manage 'creation' patterns for instances of all these things
• the meta-level issues I've raised about 'what is allowed to depend on what?', collected together in Dependency of `Algebra.Properties` on `Algebra.Bundles` or `Algebra.Structures`? Similarly: `Relation.Binary.Reasoning.*` #3046

I've come to the conclusion that we should let our module/namespace hierarchy manage this for us: (to be clarified, I think what's here still isn't quite right yet)

• Algebra.Raw is the root of a subhierarchy of individual Algebra.Raw.X modules in which the old-style RawX, and perhaps its various definitional/conservative extensions/expansions, should now live
• Algebra.Structures is the root of a subhierarchy of individual Algebra.Structures.X modules where the old-style IsX should now live, but called X, not IsX (!)
• Algebra.Bundles is...

That is,

• each individual X becomes the 'lookup key' to its various semantic components under the relevant Algebra.<semantic category> hierarchy
• when we have the occasion to put individual components of such things together, eg when building a bundle out of a raw-thing and a structure-thing, then we 'just' use qualified import to use the modules names we do at present

I would love this to work in a friction-free way, but can't help dreading some horrible viscosity issues downstream. But as usual: FYC.

[JacquesCarette]

I would vote for Algebra.Signature rather than Raw. And RawMonoid makes no sense -- it has a name as a signature, it is a PointedMagma. RawMonoid makes no sense because it would be the name also for

1. PointedSemigroup
2. LeftUnitalMagma
3. RightUnitalMagma
4. LeftUnitalSemigoup
5. RightUnitalSemigroup

Algebra.Structures made sense when it was a giant file containing "structures". For the hierarchy, Algebra.Structure makes more sense (i.e. not pluralized). Ditto for Bundle.

Have you read A Language Feature to Unbundle Data at Will? The 2018 blog post by Tom Hales reviews the problem quite well (see his complaints 7-11 which are all related). Of course, my paper was remiss in not citing Type classes for mathematics in type theory

It's also worth noting that the Rocq people (and MathComp) have resorted to meta-programming -- see Hierarchy Builder; the introducing paper can be a little hard to find. It does cite MathScheme and MMT (but not Isabelle locales!!!).

[jamesmckinna]

Apologies for RawMonoid... typing while asleep. But thanks for the lecture ;-) Its good to write this down so others don't make the same casual error.

[jamesmckinna]

[Moved to #3053]

[jamesmckinna]

Regarding the suggested reading, many thanks again for reposting. These things have come up before on specific issues, so it's good to repost, and perhaps, in addition to Vocabulary we should also have a Bibliography item...?

As to the reading itself, yes, but effectively/in practice, no. When I read it was too long ago, and my mind too different, for that experience really to be accessible. Back to the bookshelves!

[jamesmckinna]

Re: Tom Hales link. It simply points back to this Discussion item!

[JacquesCarette]

Fixed now.

[JacquesCarette]

A bit of history: seems that the RawX terminology goes back to least a 2007 version of stdlib where Nils introduced RawMonad. I'm pretty sure other uses of Raw in the library copied this naming scheme for law-less things. So this nomenclature is serious legacy!

[jamesmckinna]

As part of Vocabulary, can we lift some of the discussion of 'diamonds' out from #3053 to here?

[JacquesCarette]

I'm sure we can, but I wouldn't quite know where to start!