[Iris-Club] Fractional Monoid

[Ralf Jung]

Hi all,

I think the way the fractional monoid is defined in the appendix right
now is not perfect, and I'd like to extend that definition to cover more
use-cases that come up in my Rust stuff.

# Current definition

Right now, the members of the fractional monoid Frac(A) are pairs (q, a)
of a fraction q > 0 and a data element a \in A. A can be any set.
Composition is defined as

  (q, a) * (q', a') = (q+q', a)   if a=a'

The only frame-preserving update is

  (1, a) --> (1, b)

# The problem

For my Rust work, I'd like to have a construction that provides
fractions, while also maintaining some separation on the data elements.
Concretely, I need fractional ownership of pairs consisting of a
lockstate (unlocked, writing, reading N) and a value, and there is
interesting separation going on in the lockstate, e.g.

  reading N * reading M = reading N+M

The Frac construction above ignores any separation on A, treats it as a set.

# The solution

What I'd like to do is to let Frac(M) inherit the separation of M. The
idea is that Frac(M) is a lot like M, but we also track the fraction so
that we know when we have full ownership, and we can do any
frame-preserving update.
So, we'd have Frac(M) with the same elements as above, but

  (q, a) * (q', a') = (q+q', a*a')

We can then have the above frame-preserving update, plus:

        a --> b
  -------------------
   (q, a) --> (q, b)

The old Frac(A) now becomes Frac(Ag(A)). The equality constraint that
was baked into Frac, now arises from the use of agreement. I think this
significantly improves the overall story for fractions, and makes them
much more modular.

# The questions

In your work with Iris, did you ever encounter the need for fractions
the way I need them for Rust, something that provides the second
frame-preserving update? Would the proposed Frac(M) give you the right
separation? Did you ever encounter the need for fractions that cannot be
covered by Frac(M)?

Also, note that Ag(A) of course *could* be my really complicated
agreement construction that I presented for HOPE. But that's not
necessary here. In all cases I encountered so far, A has decidable
equality and a discrete metric, in which case Ag(A) can be constructed
in avery straight-froward way (that is actually already formalized in
the current Coq development). I call this simplified version AgDec, and
I'd like to put it into the appendix. Did you encounter the need for
agreement on types which don't have decidable equality?

Kind regards,
Ralf