Shortcomings of subevents

[YaZko]

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

[Lysxia]

The common issue with E -< F seems to be that it doesn't reflect the fact that in practice F is a sum of effects built using +', and E is one of them, so you should be able to define operations on E, lift them through the sums and reason about that.

One solution may be to replace (or wrap) +' with a type parameterized by the list of effects, looking like this:

Definition sum_of : list (Type -> Type) -> Type -> Type.

[Lysxia]

Here's a PoC to try and address the second point. The idea is to define a type class indexed by instances of -< to describe the commutation of swap with subevent.

Require Import ITree.ITree.
Require Import ITree.ITreeFacts.

(* A class of event transformations. *)
Class Swap (E : Type -> Type) : Type := swap : E ~> E.

Instance Swap_left E F `(Swap E) : Swap (E +' F) := fun _ e =>
  match e with
  | inl1 e => inl1 (swap _ e)
  | inr1 f => inr1 f
  end.
Instance Swap_right E F `(Swap F) : Swap (E +' F) := fun _ e =>
  match e with
  | inl1 e => inl1 e
  | inr1 f => inr1 (swap _ f)
  end.

(* A swappable event type *)
Variant fooE : Type -> Type :=
| Foo : bool -> fooE nat
.

Instance Swap_foo : Swap fooE := fun _ e =>
  match e with
  | Foo b => Foo (negb b)
  end.

(* A predicate class of [subevent] ([-<]) instance which behave well
   with respect to [Swap] *)
Class SwapGood (E F : Type -> Type) `(E -< F) `(Swap E) `(Swap F) : Prop :=
  swap_good : forall X (e : E X),
       swap _ (subevent _ e)
    = @subevent E F _ _ (swap _ e).

Instance SwapGoodLeft (E F G : Type -> Type) `(SwapGood E F)
  : SwapGood E (F +' G) _ _ _ := {}.
Proof.
  intros. cbv in *. congruence.
Qed.

Instance SwapGoodRight (E F G : Type -> Type) `(SwapGood E G)
  : SwapGood E (F +' G) _ _ _ := {}.
Proof.
  intros. cbv in *. congruence.
Qed.

Lemma test {E F X} `{Swap E} `{Swap F} `{E -< F} (SG : SwapGood E F _ _ _) (e : E X) :
    swap _ (@subevent E F _ _ e)
  = @subevent E F _ _ (swap _ e).
Proof.
  rewrite swap_good.
  reflexivity.
Qed.

[YaZko]

That is indeed a light-weight way to proceed that seems reasonable in this particular case, thanks for the suggestion. Despite the quite specific name Swap, it is fairly general too.

I was trying to think if this approach can be straightforwardly extended to effect morphisms in general rather than just homomorphisms, but it falls short since we need to somehow express the type resulting from the substitution of the subeffect E in the ambiant domain F, i.e. some kind of F[E <- G] for E -< F.

[Lysxia]

From our discussion just now I finally understand that by "homomorphism" you mean "endomorphism" E ~> E, as opposed to E ~> F. In that more general case we could try a four-place relation ... `{E -< E'} `{F -< F'} `{Swap E F} `{Swap F F'} (instead of three-place above ... `{E -< F} `{Swap E} `{Swap F}), expressing this commutative diagram, where arrows correspond to instances:

E -< E'
↓    ↓ Swap
F -< F'

[YaZko]

Oh sorry for the brain fart, I indeed meant endomorphism!

And right that would give something like that:

Require Import ITree.ITree.
Require Import ITree.ITreeFacts.

(* A class of event transformations. *)
Class FunctorE (E F : Type -> Type) : Type := functorE : E ~> F.

Instance FunctorE_left E F G `(FunctorE E F) : FunctorE (E +' G) (F +' G) := fun _ e =>
  match e with
  | inl1 e => inl1 (functorE _ e)
  | inr1 f => inr1 f
  end.
Instance FunctorE_right E F G `(FunctorE E F) : FunctorE (G +' E) (G +' F) := fun _ e =>
  match e with
  | inl1 e => inl1 e
  | inr1 f => inr1 (functorE _ f)
  end.

(* A functorEpable event type *)
Variant fooE : Type -> Type :=
| Foo : bool -> fooE nat
.

Variant barE : Type -> Type :=
| Bar : nat -> barE nat
.

Instance FunctorE_foo : FunctorE fooE barE := fun _ e =>
  match e with
  | Foo b => if b then Bar 1 else Bar 0
  end.

(* A predicate class of [subevent] ([-<]) instance which behave well
   with respect to [FunctorE] *)
Class FunctorEGood (E E' F F' : Type -> Type) `(E -< F) `(E' -< F') `(FunctorE E E') `(FunctorE F F') : Prop :=
  functorE_good : forall X (e : E X),
    functorE _ (@subevent E F _ _ e)
    = @subevent E' F' _ _ (functorE _ e).

Instance FunctorEGoodLeft (E E' F F' G : Type -> Type) `(FunctorEGood E E' F F')
  : FunctorEGood E E' (F +' G) (F' +' G) _ _ _ _ := {}.
Proof.
  intros. cbv in *. congruence.
Qed.

Instance FunctorEGoodRight (E E' F F' G : Type -> Type) `(FunctorEGood E E' F F')
  : FunctorEGood E E' (G +' F) (G +' F') _ _ _ _ := {}.
Proof.
  intros. cbv in *. congruence.
Qed.

Lemma test {E E' F F' X}
      `{FunctorE E E'} `{FunctorE F F'}
      `{E -< F} `{E' -< F'}
      (SG : FunctorEGood E E' F F' _ _ _ _) (e : E X) :
    functorE _ (@subevent E F _ _ e)
  = @subevent E' F' _ _ (functorE _ e).
Proof.
  rewrite functorE_good.
  reflexivity.
Qed.

That actually looks alright, I'll try toying with it asap!