Record hierarchies

[uniwuni]

Since some kind of record hierarchy is definitely required for, say, algebra, category theory, topology, and pretty much any other sort of mathematics, the implementation details need some consideration.

Usually, there are at least two separate kinds of records related to a single kind of structure:
One that parameterizes over all the data involved in the structure, e.g.

data isSemigroup (A : Type) (_*_ : A -> A -> A) where
  field is-associative : ...
  ...

which is needed to state that a specific operation does conform to laws required for a structure, as well as another one that parameterizes only over the involved type:

data SemigroupOn (A : Type) where
  field
    _*_ : A -> A -> A
    is-associative : ...
  ...

which is mainly required to avoid clutter in type signatures and allow for more general theorems.

One probably needs both of these types, but which approach should be used primarily?

It does get even more complicated when considering "inheritance"/nested records: given the semigroup definitions above, how exactly would one extend these to monoids? Would MonoidOn A have SemigroupOn A as a field, or would it include the _*_ operator as a field as well as a proof of isMonoid A _*_?

The questions do not stop there - for example, given that it is unique, should the unit of a monoid be included in the type signature of isMonoid? That's why this issue is meant as a place to collect ideas on how to find solutions to all of these topics.

[plt-amy]

Just as an aesthetic matter, I kinda hate having the operations be parameters to the record. Imagine the size of a theorem that's parametrised over a ring, or a Heyting algebra!

As a more practical justification for this, in univalent mathematics, we want equality of "structured types" to be homomorphic equivalence - the Structure Identity Principle - and our current infra for that requires that the structure be a family Type -> Type. Sure we can adapt the isFoo to a FooOn, but should we have to?

[uniwuni]

I don't know, I think "there exists S : Group Int such that S.* = +" is pretty ugly to write as well, and sometimes there's a need for these statements in more general contexts, like for example in the Eckmann-Hilton argument

[JacquesCarette]

This whole issue of parameters vs fields, bundling vs unbundling, is a well-known design problem in libraries. I've dabbled around it. There's an active discussion of that design for stdlib. Arend seems nice here.

Yes, the SIP says that none of this matters. Unfortunately the "engineering" work so adapt Agda (plain or cubical) to deal gracefully with the SIP has not yet been done.

[uniwuni]

Interesting and pretty impressive tool - it'd force one to abandon the literate Agda approach though, at least to some degree. I don't know how much effort it would take to figure out how to connect code and text in a more modular way, but to me it'd be worth consideration at least.

[plt-amy]

A thought is that we could potentially only write the unbundled version (i.e. isSemigroup from the OP), and generate the bundled versions with reflection.

Sadly you can't add new record definitions with reflection, but I think we could generate Σ types and named projections. @TOTBWF does that check out?

[plt-amy]

Similarly I assume we could write reflection helpers that could automatically generate Structure and SNS definitions from the unbundled record definitions.

[adamse]

Somewhat related discussion: https://lists.chalmers.se/pipermail/agda/2020/011747.html

[JacquesCarette]

Note: I am not at all suggesting that my tools be adopted here. Think of them as an exploration of the design space, food for thought.

To expand on @adamse 's comment for those too lazy to read the thread: Jesper confirms that generating Σ sigma types and explicitly named projections is possible, the other direction is not.

[bowtochris]

Every approach is obnoxious, of course. I prefer the approach like
data isRing (A : Type)(plus, mult:A -> A -> A)(0, 1:A) where field is-group : isGroup A plus 0 is-monoid : isMonoid A mult 1 is-distributive-left : ... ...

because it makes defining structures that inherit from multiple other structures easier. Like, in my pet project, I defined a group as a loop and a monoid on the same set and operation, so isGroup just had the fields isLoop and isMonoid and that's it.

The alternative, a GroupOn A having the fields LoopOn A and MonoidOn A with the operations and units being equal doesn't work for me because I don't want the operation to be propositionally equal. I want them to be judgementally equal.

[JacquesCarette]

I'm back, because of the call on twitter. I've more than dabbled around this - I've had 2 PhD students write their thesis around the topic: Yasmine Sharoda and Musa Al-hassy. Yasmine's tools are available in a separate repo.

In both cases, I would recommend looking at their material for their defense as a good entry point.

It's fun to look at Musa's early prototype written in e-lisp. It generates quite a lot of Agda (as does Yasmine's).

In Yasmine's notation, here is what the hierarchy up to Monoid looks like:

module Monoids where

Map plus = {op to +}
Map zero = {e to 0}
Map one = {e to 1}
Map plus-zero = {op to + ; e to 0}
Map additive = { e to 0 ; op to + }

Theory Empty = {} 
Carrier = extend Empty {A : Set}
Pointed = extend Carrier {e : A}
PointedZero = rename Pointed zero
PointedOne  = rename Pointed one
Magma = extend Carrier {op : A -> A -> A}
AdditiveMagma = rename Magma plus

PointedMagma = combine Pointed {} Magma {} over Carrier
Pointed0Magma = combine PointedZero {} PointedMagma zero over Pointed
PointedPlusMagma = combine AdditiveMagma {} PointedMagma plus over Magma
AdditivePointedMagma = combine Pointed0Magma plus PointedPlusMagma zero over PointedMagma

Semigroup = extend Magma {associative_op : {x y z : A} -> op (op x y) z == op x (op y z) }
AdditiveSemigroup = combine AdditiveMagma {} Semigroup plus over Magma

PointedSemigroup = combine Semigroup {} PointedMagma {} over Magma
APointedSG1 = combine PointedSemigroup plus-zero AdditiveSemigroup {} over Semigroup
APointedSG2 = combine PointedSemigroup plus-zero AdditivePointedMagma {} over PointedMagma
AdditivePointedSemigroup = combine APointedSG1 {} APointedSG2 {} over PointedSemigroup

LeftUnital = extend PointedMagma { lunit_e : {x : A} -> op e x == x }
RightUnital = extend PointedMagma { runit_e : {x : A} -> op x e == x }
AdditiveLeftUnital = combine AdditivePointedMagma {} LeftUnital plus-zero over PointedMagma 
AdditiveRightUnital = combine AdditivePointedMagma {} RightUnital plus-zero over PointedMagma 

Unital = combine LeftUnital {} RightUnital {} over PointedMagma
AUnital1 = combine AdditiveLeftUnital {} Unital plus-zero over LeftUnital
AUnital2 = combine AdditiveRightUnital {} Unital plus-zero over RightUnital 
AdditiveUnital = combine AUnital1 {} AUnital2 {} over Unital 
-- AdditiveUnital = combine AdditivePointedMagma {} Unital plus-zero over PointedMagma

idUnital = id from AdditiveRightUnital to AdditiveUnital


Monoid = combine Unital {} PointedSemigroup {} over PointedMagma 

when unwound, that single line for LeftUnital generates 127 lines of Agda.

Again, I'm not saying that this is the way to do it. But it is one part of what is known about the design space.

[plt-amy]

A few key points I've thought about:

• The "unbundled" approach, with the operations in the record telescope, is preferable in our setting because it lets us say that two operations are the same up to defn. eq., rather than a path. Especially since there's no pattern-matching on refl to make using equalities simpler, that's a big win. This also lets us share operations coherently in structures that are not h-sets, without having to add extra coherences.

• Any automatic approach using an external tool would have to support "the 1lab usecase": support literate mode programming, and, automatically syntax highlighting and hyperlinking of the source. Very possibly, the Agda-generated anchors would have to be postprocessed to make sure identifier hyperlinks point to the right place in the output page.

• Reflection based approaches have the downside of having to write out the names of every identifier in a macro call. Acceptable for stuff like semigroups, but consider a 2-monoid: operation, unit, two identity paths, an associativity path, one pentagon identity, two triangle identities, groupoid truncation, in addition to the type name itself.

[TOTBWF]

Yeah, that's an accurate description of the situation. I did some research into what prevents the generation of records: it seems that the scope-checker needs to know what names exists before macro expansion, which means that any sort of unquoteRecord primitive would have to provide the names of all of the fields [1, 2, 3].

WRT to iterated sigmas, I'm always a bit leery of them. Once you add large numbers of fields, the compile time performance can really suffer. Furthermore, we would run into the exact same problems with the scope-checker + macros. That's not to say it wouldn't work, just that we ought to seriously consider the ratio of what we are giving up vs. what we are getting.

@plt-amy suggested a great idea: Adding something akin to ghc -F that lets us run a custom preprocessor [4], or add
something akin to ghc plugins [5]. However, this is quite a bit of work, and I don't think it's a good idea to block anyone on this.

For now, I think the best option may to go with iterated sigma types as our "core" abstraction, and provide records as a nice interface for working with various representations. From a purely selfish perspective, I'd like to experiment with some ideas regarding reflection, and using the iterated sigmas is table stakes for doing so.

References

• https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Creating.20new.20datatypes.20with.20reflection/near/231312022
• Allow metaprogramming to generate top level definitions other than functions agda/agda#3699
• [ re #5399 #3699 ] Add primitives tcDeclareData and tcDefineData agda/agda#5507
• https://downloads.haskell.org/ghc/latest/docs/html/users_guide/phases.html#pre-processor
• https://downloads.haskell.org/ghc/latest/docs/html/users_guide/extending_ghc.html?highlight=plugin#compiler-plugins

[L-TChen]

Furthermore, we would run into the exact same problems with the scope-checker + macros.

If Agda checks the scope per block of code instead of a file, then it should be able to introduce indefinitely many names into the scope after expanding a macro. I feel mixed about introducing names implicitly, but it is probably okay for modules.

[plt-amy]

Here's the design I came up with:

https://github.com/plt-amy/cubical-1lab/blob/404d451798e230b7fbce9acc2fbd0c84157b7fd4/src/Algebra/Monoid.lagda.md (rendered: https://cubical.1lab.dev/Algebra.Monoid.html#2847)

@TOTBWF @uniwuni Your thoughts on this?

[uniwuni]

This looks pretty good to me! I'd have another record for magmas in general though, only containing the is-set property. Also, I think renaming associative to \star-associative would simplify the naming for structures with multiple operations.

[plt-amy]

Right, we can paint the shed another colour later 😉 I think it's a bit unfortunate that we still need to make the isMonoid, MonoidOn and Monoid≃ records by hand, but I'm not sure that there's much that can be done about this (especially internally), but I think overall this interface is going to be friendly enough to Do Maths With and it's very tractable to automatically SIP with.

[JacquesCarette]

Looks really good. And is indeed what Musa Al-hassy was saying in his PhD thesis (though he wasn't as clear about it, sigh).

The underlying vision is to look at telescopes with a moveable 'focus', which tells you what goes in the parameters and what is fields, while also seeing the members of telescopes as themselves being subject to bundling/unbundling. So telescopes should really be seen as marked trees (with ordered children). Well, marked DAGs because of dependency and sharing.

When you instantiate is to things that can be said in generalized algebraic theories, and draw up examples, you get a collection of records very much as you have them.

One of the additional observations of Musa's thesis is that from such focused telescopes, one then gets different results by applying different operators, namely lambda, Pi and Sigma that transform telescopes into other things. [There is tons of category theory all over, but that's not how category theorists traditionally see this. Too much focus on the implementations (aka presheaves) instead of on the declarations (the fibrational structure of the category of contexts).