Description
As has been discussed several times, the current support for subevents seems insufficient for practical use. This issue details a couple of concrete difficulties it raised as we used them in the Vellvm project, and suggests a potential line of action. The proposed solution is quite vague and meant as a start for discussions.
-------------------------- First concrete issue --------------------------
The first difficulty is in the definition of handlers in a fairly large ambient context of events.
Consider we want to interpret into the state monad a set of events LocalE. We hence have a handler:
Definition handle_Local {E} : (LocalE k v) ~> stateT map (itree E) := ...
Now we would like to run the corresponding interpreter. However, currently, the definition of this interpreter has to be tailored extremely closely to the structure of the ambiant universe of events. More concretely, events being associated to the right, we are currently working in a context of the form F +' G +' LocalE +' H for some concrete values of F, G, H.
We hence need the following definition:
Section PARAMS.
Variable (E F G : Type -> Type).
Definition E_trigger {M} : forall R, E R -> (stateT M (itree (E +' F +' G)) R) :=
fun R e m => r <- trigger e ;; ret (m, r).
Definition F_trigger {M} : forall R, F R -> (stateT M (itree (E +' F +' G)) R) :=
fun R e m => r <- trigger e ;; ret (m, r).
Definition G_trigger {M} : forall R , G R -> (stateT M (itree (E +' F +' G)) R) :=
fun R e m => r <- trigger e ;; ret (m, r).
Definition run_local `{FailureE -< E +' F +' G} : itree (E +' F +' (LocalE k v) +' G) ~> stateT map (itree (E +' F +' G)) :=
interp_state (case_ E_trigger (case_ F_trigger (case_ handle_local G_trigger))).
End PARAMS.
Not only is this definition naturally unsatisfactory, but it breaks if we add or remove a family of events in the wrong place during a refactoring, and cannot be used in another context, something that turns out to be useful.
It hence seems that a first "feature request` would be to have a systematic way to extend handlers to subsets of events.
-------------------------- Second concrete issue --------------------------
Now the second difficulty, which very much relates to the first, appears when we start proving transformations on the trees. Consider a typeclass Swap A := {| swap: A -> A |} of types equipped with an endomorphism swapping the names of two identifiers fixed at the top level.
The instance for LocalE is non-trivial, since its events take identifiers as arguments. On other domains of events, it is the identity. We can of course define an instance for +'.
On itrees, to swap is defined as swap t := map swap (translate swap t).
Now one thing that we need to prove is that swap commute with the triggering of the subevents we use in the semantics. That is ideally that swap (@trigger E X (subevent e)) \cong @trigger E X (subevent (swap e)), assuming Swap E and some things about X.
However this cannot be proved, since F -< E gives us an embedding from F into E, but tells us nothing about this image of F in E.
In order to prove such a lemma, we actually need to fix not only F, but also E. Worse, the proof relies actively on the specific instance for F -< E that gets inferred, that is essentially relies on the fact that ReSum_inl and ReSum_inr can be inversed.
This leads to a significant amount of ad-hoc lemmas with duplicated proofs.
-------------------------- Feature request? --------------------------
To sum up, currently, the -< typeclass does not expose enough information to define generic constructs and prove generic lemmas about them. We would in particular like to be able: given h:E ~> M and E -< F, derive F ~> M that should intuitively behave as h over the embedding of E into F, and as some kind of identity otherwise.
This seems to suggest notably that an instance E -< F should not only provide an embedding E -> F, but also a membership test is_in_E: F -> bool
Since the handler goes into a monad in general, it is not exactly an identity that we need. Looking back at our first issue, we need the monad to support some generalized way of triggering the event into the monad.
This would be a typeclass Events E M := {trigger: E ~> M} that has the obvious instance for itree E, as well as instances for the monad transformers we support, typically a {Events E M} -> {Events E (stateT _ M}}.
Finally we naturally need the instances to come with reasonnable reasoning principle to adress the second issue described above.
Best,
Yannick