[Iris-Club] Two Monoid Questions

Ralf Jung jung at mpi-sws.org
Tue Aug 13 12:46:49 CEST 2019


> I'm not sure that it even makes sense to use a canonical structure or a type
> class to infer the "models" relation. I would suppose it's possible that on the
> same types you may want to use a different "models" relations depending on the
> use-case.
> As such, I would suppose that the first option (namely, having the types +
> relation unbundled) makes most sense. Most of the time, you would do something
> like:
>   Definition myR := authR ...
> And if you use myR, Coq can infer the "models" relation from that.
> The thing that I'm a bit more worried about is that in the general setting, the
> types A and V will be OFEs, the "models" relation will be a step-indexed
> relation, and should be non-expansive.
> Without the type sProp of step-indexed propositions this will all be very
> annoying to use. Maybe we should add that type someday.

Yeah, we would likely need that type for the step-indexed version of this.

>> Hm, this is an interesting thought. We do not permit composing two
>> authoritatives anyway, 
> We actually do: https://gitlab.mpi-sws.org/iris/iris/merge_requests/215

Good point, I forgot about that.  But we can just use agreement for the predicate.

However, I think the predicate won't do for another reason: it can be very
useful to know, given ownership of some fragment, that this is a (partial) view
for *some* authoritative element.  For example, this proposal [1] for an
authoritative partial bijection exploits this for a lemma like

  Lemma in_bij_agree γ L (a a' : A) (b b' : B) :
    own_bij γ L -∗
    in_bij γ a b -∗
    in_bij γ a' b' -∗
    ⌜a = a' ↔ b = b'⌝.


So, I think we want the predicate/relation encoded in the type, not just the
authoritative element.  And that will mean making it a relation so that the
"full view" can change.

Kind regards,

More information about the Iris-Club mailing list