GitLab

Right now, Iris is instantiated with a single global monoid. As described in the appendix, we can easily use the product monoid to have multiple different monoids available in Iris, but this still requires knowing the exact set of all monoids we will need up-front, before instantiating the logic. That's not nice.

I see two possible solutions.

The "any" monoid

We could have a monoid of the form "\Sigma (A: Type) {RA A}. A". This is a monoid that can be "any" monoid. However, doing that in Coq would get very hairy. We would have to require equality of the types and RAs in the composition, and somehow transport the actual data in A over that equality to even compose the pieces. I think FCSL is doing something like this, but they assume all sorts of classical axioms. We would probably want at least function extensionality and Axiom K.

The "all" monoid

When I was visiting @robbertkrebbers , we talked about indexed products a lot as they impose some interesting challenges when done in Coq, where we don't want to assume the axiom of choice. We agreed that for example, it would be nice to have he set of all STS graphs + token assignments in the index set, so that we could actually have all STS monoids at once, rather than having to add every single STS monoid to the global monoid individually.

That had me thinking, could it be possible to index the product by monoids? Essentially, replace the \Sigma above by a \Pi. That would be the monoid of all monoids, with the index defining the monoid structure at that position. We just do everything pointwise, so there should be no trouble with inhomogenous equality or anything like that. As long as we make sure that a module always uses the same index, and nobody reasons about equality of indices, we should be good - right? Or did I miss anything here?

@janno, @swasey, we also talked about this problem at some point, so you're probably also interested in this.