Sum CMRA / CMRA without core
We would like to support a sensible CMRA structure on sums. For example, we could use a sum CMRA to express one_shot X
as exclC unitC + ag X
. We could also express the disposable monoid using sums.
Right now, the CMRA structure on sums does not make much sense because both summands need to have a core. It is thus impossible to do a frame-preserving update from inl a
to inr b
. For sums to work out nicely, we need a way to have summands without a unit.
@robbertkrebbers and me agreed that the most promising way forward is to get rid of the core in the CMRA axioms, and instead add a typeclass for "CMRAs that also have a core". There should not be significant performance trouble because the iFunctor
will bundle the core of the user CMRA. The main open question is whether the loss of reflexivity in the CMRA inclusion will be a problem.