Syntax modules

[fredrik-bakke]

I'm curious about opinions and input on this one @EgbertRijke @VojtechStep @lowasser. This is the kind of thing I had in mind when I mentioned syntax modules for wild categories the other day.

If you add the below module, then you can "open" the syntax elsewhere using open operator-syntax-Quasigroup Q, to access these operators for your chosen quasigroup Q, instead of using private definitions as you do currently.

### Quasigroup operator syntax

```agda
module
  operator-syntax-Quasigroup
  {l : Level} (Q : Quasigroup l)
  where

  _*_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _*_ = mul-Quasigroup Q

  _l/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _l/_ = left-div-Quasigroup Q

  _r/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _r/_ = right-div-Quasigroup Q
```

Originally posted by @fredrik-bakke in #1330 (comment)

EDIT: I would actually prefer the following syntax

module
  structure-syntax-Quasigroup
  {l : Level} (Q : Quasigroup l)
  where

  _*_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _*_ = mul-Quasigroup Q

  _⧵_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _⧵_ = left-div-Quasigroup Q

  _∕_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
  _∕_ = right-div-Quasigroup Q

[VojtechStep]

Related to #768. I remember discussing this with Egbert in September '23, where we identified two issues:

1. printing those things in goals is finicky. If the syntax is an unapplied function like _*_ or not a function like Q', then it gets printed as operator-syntax-Quasigroup._*_ Q and operator-syntax-Quasigroup.Q' Q. We didn't find a way to unfold these definitions. If the syntax is an applied function, such as e * x, then the syntax may be inlined. For _*_ = mul-Quasigroup Q, the syntax is inlined (because we're using --auto-inline and it meets the criteria for automatic inlining). This is probably what we want, but it's unfortunate that it gets expanded even if you open the syntax, potentially with renaming, because it's harder to see how theorems about an unapplied function (unexpanded) relate to applications of the function (expanded). If the syntax is not inlined (e.g. by using the NOINLINE pragma), then even its applied form will still use the symbol, or possibly a different one if you open ... renaming (_*_ to something-else); though if you don't have the syntax module open, then printing mixfix operators will get confused, because it has the extra module parameters, so if you use e * x it will look like (Q operator-syntax-Quasigroup.* e) x outside. All that is to say that we probably need to decide if we expect syntax modules to be used pervasively (then the syntax should probably be NOINLINE; this could potentially have performance implications, auto inlining was enabled for a reason, but I can't tell if these cases will result in anything noticable), or used rarely (in which case the long names are the primary ones, but we can't get non-functions and unapplied functions to cooperate)
2. the same issue that lead to abandoning usage of named modules in the first place: you can't extend them, so you either end up with a hierarchy of modules that you want to open at use site to have readable goals (see previous point; at the time strongly rejected by @EgbertRijke), or you only define one module, but then modules participating in its definition don't have access to the syntax because of circular dependencies. This is the "modules are not namespaces" discussion that comes up from time to time

[fredrik-bakke]

just so we are on the same page, we do not like the notation Q' for the underlying type of a quasigroup.

[fredrik-bakke]

I wonder if the performance penalty of NOINLINE is mitigated to some extent by --lossy-unification

[fredrik-bakke]

Regarding your second point, do I understand correctly that you see an issue with something like the following scenario?

Consider the structure of a group, then we can define a group syntax structure-syntax-Group for the basic structure: e, _*_, and _⁻¹. If we later want to add, say, the commutator operator ［_，_］, then we will have to define a new syntax module for it commutator-syntax-Group, or add every notation we will commonly use all at once in structure-syntax-Group.

It seems to me that, for the limited use case of modules for syntax, this is a very minor issue, and it is resolved by having the convention that every new syntax is added to a new syntax module with an appropriate name to describe what the syntax is for.

[fredrik-bakke]

To be clear, this means my previous suggestion for a syntax module name was bad. We shouldn't have a module called operator-syntax-Quasigroup; that is not disambiguative enough.

[fredrik-bakke]

I agree that your first point is an issue, but I believe the benefits outweigh the drawbacks, and using the NOINLINE pragma seems like a valid route. Notice also that there are already common mismatches between goals and definitions due to our use of iterated Sigma types.

[fredrik-bakke]

Just to elaborate a bit further with another example. For something like wild category theory, I think a syntax like this will be essential for raising the usability of the formalizations to a level where expressions aren't just drowned in Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory Noncoherent-ω-Precategory.

I would envision a structure syntax module like the following, this example having identity morphisms, composition of 1-morphisms, composition of 2-morphisms, horizontal composition of 2-morphisms, and whiskering of 2-morphisms with 1-morphisms and vice versa.

module
  structure-syntax-Noncoherent-ω-Precategory
  {l1 l2 : Level} (𝒞 : Noncoherent-ω-Precategory l1 l2)
  where

  id₁ :
    {x : obj-Noncoherent-ω-Precategory 𝒞} →
    hom-Noncoherent-ω-Precategory 𝒞 x x
  id₁ = id-hom-Noncoherent-ω-Precategory 𝒞

  _∘₁_ :
    {x y z : obj-Noncoherent-ω-Precategory 𝒞} →
    hom-Noncoherent-ω-Precategory 𝒞 y z →
    hom-Noncoherent-ω-Precategory 𝒞 x y →
    hom-Noncoherent-ω-Precategory 𝒞 x z
  _∘₁_ = comp-hom-Noncoherent-ω-Precategory 𝒞

  _∘₂_ :
    {x y : obj-Noncoherent-ω-Precategory 𝒞}
    {f g h : hom-Noncoherent-ω-Precategory 𝒞 x y} →
    2-hom-Noncoherent-ω-Precategory 𝒞 g h →
    2-hom-Noncoherent-ω-Precategory 𝒞 f g →
    2-hom-Noncoherent-ω-Precategory 𝒞 f h
  _∘₂_ =
    comp-2-hom-Noncoherent-ω-Precategory 𝒞

  _∙₂_ :
    {x y z : obj-Noncoherent-ω-Precategory} →
    {g g' : hom-Noncoherent-ω-Precategory y z}
    {f f' : hom-Noncoherent-ω-Precategory x y} →
    2-hom-Noncoherent-ω-Precategory g g' →
    2-hom-Noncoherent-ω-Precategory f f' →
    2-hom-Noncoherent-ω-Precategory
      ( comp-hom-Noncoherent-ω-Precategory g f)
      ( comp-hom-Noncoherent-ω-Precategory g' f')
  _∙₂_ = horizontal-comp-2-hom-Noncoherent-ω-Precategory 𝒞

  _₂·₁_ : ...

  _₁·₂_ : ...

[VojtechStep]

Let me preface this by saying that I'm playing the devil's advocate. The two points I raised aren't necessarily my issues, I'm only arguing from the point of view of the current library's approach to code organization.

The module vs namespace issue boils down to the question of how we split code into files. You propose a module defining syntax for over 5 definitions. Some of those are probably not just aliases for fields of the structure, but are derived notions (in this example whiskering would be horizontal composition of an n+1 cell and an identity on a composable n cell, right?). Then they should be defined in a separate file on whiskering. And that's where you encounter the problem: you either have a syntax module per file, and if you want to make sense of e.g. biwhiskering you would need to open three syntax modules (base, left whiskering, right whiskering), or you have a master syntax module which can't be used by any other file which participates in defining a symbol aliased by the syntax.

Then there's the issue with algebraic hierarchies. When we currently define one structure as an instance of another with extra stuff (like a monoid being a unital semigroup), we write out all the deep accessors, not only because it makes the code using it easier to read, but because jumping to definition takes you to the file about monoids, not semigroups. If we bring syntax modules into the mix, we either a) reopen the syntax for working with the underlying structure, which means go to definition on operators goes too deep, b) don't reopen the underlying syntax and only define syntax for the new parts, which means use sites will want to open a hierarchy of syntax modules and go to definition still goes too deep, or c) don't reopen the underlying syntax, but manually copy over the definitions, which means that users will only have to open one module, and go to definition takes you to the right file, but we have to copy and paste code, which is yucky.

[fredrik-bakke]

Random thought today:

Using instance arguments it seems possible, using a syntax module, to define dimension polymorphic composition operators on wild higher categories. I.e., it should be possible to have an operator _∘_ for composition of n-cells in 𝒞 with arbitrary n, and the same for hom and _∙_ (Unicode symbols TBD).

[VojtechStep]

Regarding the "we don't like Q' syntax for the underlying type", I recently came across let bindings in module telescopes, e.g.

module _
  {l : Level} (L : Loop l)
  (let Q = quasigroup-Loop L)
  (let Q' = type-Quasigroup Q)
  where

which seem to be completely transparent for the outside world — all occurrences of Q' look like type-Quasigroup (quasigroup-Loop L) when printing goals. As far as I'm concerned that fixes the biggest problem with private definitions from the issue I linked above.

[EgbertRijke]

Has this proposal been tested when more than one quasigroup/noncoherent category is around? We should avoid making some notational setup that just breaks on the first occasion you try to do something substantial (i.e., do something more than just making a basic definition that involves only one instance of the structure).

[VojtechStep]

If you want to use the notation for multiple objects of the same type, you can either

1. rename some of the symbols you're using

_ = {! Write a * b and x # y !}
  where
    open structure-syntax-Quasigroup Q
    open structure-syntax-Quasigroup R renaming (_*_ to _#_)

or

2. alias the syntax to a named module

_ = {! Write a Q.* b and x R.* y !}
  where
    module Q = open structure-syntax-Quasigroup Q
    module R = open structure-syntax-Quasigroup R