Mechanize the Algebra hierarchy

[Taneb]

Many of the modules under Algebra (e.g. Algebra.Structures, Algebra.Bundles, Algebra.Morphism.Structures...) are highly structured and repetitive. This makes it a lot of work to add something new, and very easy to miss things. We should come up with a way to mechanize this and generate this portion of the library from a more concise form somehow.

Considerations

• Concision: we want to be able to generate large amounts of the library's functionality from a small specification
• Completeness: we want to take care that anything we want in these modules, we can still have in these modules.
• Ease of understanding: the documentation of this library, such as it is, is in the form of source code listings. We want users of the library to still be able to figure out what we provide
• Ease of installation: the library is generally installed by copying it verbatim somewhere onto the system. We don't have a way to run, say, a Haskell program at installation time.
• Extensibility: if we want to add a new form of algebraic structure, we should be able to do so easily. If we want to add a new expression of algebraic structures (e.g. morphism bundles, or finite algebraic structures), we should be able to do that easily also.

Current state of affairs

We have three modules of "structures", containing records of laws for various algebraic structures, parameterized by their equivalence relation and operations. We have three modules of "bundles" containing records bundling the equivalence relation, operations, and the law structure, and three modules of "raw bundles" which omit the law structure. We have three modules of morphism structure, each of which is parameterized on the raw bundle. We have many modules of various properties of structures and morphisms, which may be harder to mechanize.

[jamesmckinna]

Two comments, not (entirely; or even, at all ;-)) tongue-in-cheek:

• milestone hypothetical-rewrite!? cf. [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252 , [DRY] defining concrete instances of RawX bundles #2255 , [DRY] why is _≉_ defined both for Algebra.Bundles.Raw.RawX bundles, and via Setoid instances, for Algebra.Bundles.X? #2274
• @JacquesCarette !?

[JacquesCarette]

I obviously agree emphatically with this. And, to a certain extent, this is roughly the work that Yasmine did for her Ph.D. thesis. If you couple it with the produce-documented-human-readable-code that Drasil can do, in theory I have the needed pieces in hand to do this.

In practice, these pieces are not (yet) integrated.

I would propose that we first implement this as a pre-processor. The published agda-stdlib would contain, in part, output from that pre-processor. This could be done immediately.

Then we could abstract out the features that we need to make it into a language feature.

Pinging @TOTBWF as I think he's quite interested in things like this. (Ok, what's described here is probably "baby steps" for what @TOTBWF really is interested in, but it does seem to be in a compatible direction.)

[Taneb]

Is what Drasil's been working on anywhere where I can read it?

[JacquesCarette]

Of course: Drasil . Under Papers/WellUnderstood is our most recent write-up. The wiki also have a wealth of information.

[TOTBWF]

Just getting around to this: I think the way forward is to patch Agda to have a more refined form of what I outlined at WITS '22, where record types are extended with a telescope that tracks some definitional equalities for fields. cooltt already has a version of this, and the implementation path seems pretty clear. Once I have some more time I can write up a more coherent proposal.

[jamesmckinna]

@TOTBWF Link to your WITS talk? The workshop site offers no clues...

[TOTBWF]

It's available here, but I'll also summarize the relevant bits, as I'm sure we all know the problem quite well 😁

The original idea in cooltt was that we already had enough definitional machinery laying around to implement a definitional singleton type; IE: a type Sing A a whose only element is definitionally a. This lets you start definitionally constraining fields of a record type by wrapping them in Sing. As an example, we could write Monoid-on as

record Monoid-on (A : Type) : Type where
  field
    Carrier : Sing Type A
    ...

This doesn't buy you much as is, but cooltt has a bit of elaborator magic that transforms the notation Monoid [ Carrier .= Nat ] into one of these record types (note that cooltt also has anonymous records). This is kind of neat, as you only need to write the bundled Monoid, and you get the unbundled bits for free by adding singleton types after the fact.

A lot of this pretty specific to this one implementation, but there's a kernel of a bigger idea in there. Namely, we can control bundling by carrying around a telescope of definitional equality constraints with a record type. There are a couple of ways to realize this, but I think the cleanest is to change the record type former to take in a telescope of values that correspond to some subset of the record fields. This would let us write things like Monoid [ Carrier .= Nat ] from before without requiring elaborator hacks. Next, you modify the introduction rule for records to check that any fields that show up in this telescope are definitionally equal to the corresponding value. Finally, when you project out of a neutral element of a record type, you check the list of definitional constraints for the field, and then unify the projection against the value if it is present.

I'm not that familiar with the ins and outs of the Agda codebase, but none of this should be problematic at all. The only part that might be a bit tricky is subtyping those telescopes, but it shouldn't be particularly difficult.

[JacquesCarette]

This is where we want to loop in people like @jespercockx - who I guess must have been at that talk.

[jespercockx]

While I am very sympathetic to the stated goals here, I am a bit wary of proposing a change to Agda. In the past we have been quite eager to extend Agda with more features and this is now starting to take its cost in terms on maintenance of the codebase and integration of all these features. So realistically speaking, if we want to add something like this to Agda we would first need to increase our developer team - not just to maintain the feature itself but also integrate it with all of Agda's other features.

[TOTBWF]

Completely understandable: you all have a very hard and important job, and I definitely do not want to make it harder!
I would definitely be interested in stepping up to the plate later in the year, but I unfortunately do not have the time until June at the earliest.

[JacquesCarette]

(Warning: airing a bit of frustration.) Agda seems to be a playground for type theory ideas, and it keeps growing in that sense, by adding various new flags and modalities and ... That's great for some people. Who loses out? People who are actually trying to use Agda as a system on which to base large libraries. Very few features have lately been implemented that help that. And the understandable desire to not make the maintenance burden worse means that library developers are forced to write silly amounts of boilerplate because Agda lacks the features to do otherwise.

So we may end up being forced to be pragmatic and create meta-agda instead, following MetaCoq (MetaRocq?). That seems sub-optimal, but it would allow for progress.