All relations are now parameterized by a relation L on labels, encompassing hence at once the itree-style relational postcondition passed to eutt, as well as the generalization rutt allowing to map distinct events one to another.
Currently, the type label reflects through a type parameter the signature of computations it applies to, but not its return type. It was coined this way to avoid awkward type transports when considering transitions in bind constructions, but has the drawbacks of making the relational specification L awkward: it is not aware of the return type specifically.
Additionally, having all baked into a single relation is sometimes weird: while the relation on val labels certainly must change when running a cut rule, the part on obs and taumust be invariant.
TODO: revisit these tradeoff. Expose the return type in the type of labels? Explicitly break relations into a val relation and an event relation?
All relations are now parameterized by a relation
L
on labels, encompassing hence at once the itree-style relational postcondition passed toeutt
, as well as the generalizationrutt
allowing to map distinct events one to another.Currently, the type
label
reflects through a type parameter the signature of computations it applies to, but not its return type. It was coined this way to avoid awkward type transports when considering transitions inbind
constructions, but has the drawbacks of making the relational specificationL
awkward: it is not aware of the return type specifically.Additionally, having all baked into a single relation is sometimes weird: while the relation on
val
labels certainly must change when running a cut rule, the part onobs
andtau
must be invariant.TODO: revisit these tradeoff. Expose the return type in the type of labels? Explicitly break relations into a
val
relation and an event relation?