8
$\begingroup$

I had a question on subtyping in the paper "An Effect System for Algebraic Effects and Handlers". I was wondering why there isn't a subtyping rule for adding effects on both sides of a handler type, something like this:

$$ \frac{ }{ T!A \;\Rightarrow\; R!B \;\leqslant\; T!(A \cup C) \;\Rightarrow \;R!(B \cup C) } $$

This would be useful when apply a variable with a handler type to a computation with more effects than the handler type has in its left side.

You can add effects to both sides of a handler type using the typing rule for handlers, but that won't work for variables. For example when the handler is an argument to a function.

$\endgroup$
9
$\begingroup$

I'm surprised we don't get this question more often, for Andrej and I have considered adding this rule for quite some time and believed to have proven its correctness. But in the end, it turned out to be false, at least in a call-by-value setting (I have heard it plays out nicer in call-by-push-value).

Consider the state handler, described on top of page 24 of the same paper, which takes a stateful computation of type $B$ on state $A$ and transforms it into a pure function from $A$ to $B$. Its type is $$B!\{\mathtt{lookup},\mathtt{update}\} \Rightarrow (A \to B ! \emptyset) ! \emptyset$$ Note the two empty sets on the right hand side. The first states that the resulting function is pure, the second one that there no effects occur when producing this function.

Now assume that we apply the handler to a computation that may call some other effects $\Delta$ besides $\mathtt{lookup}$ and $\mathtt{update}$. Applying the suggested rule, you would get the type $$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \emptyset) ! \Delta$$ but in fact, the correct type is $$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \Delta) ! \Delta$$ as the unhandled effects $\Delta$ may occur before producing the function or after calling it.

$\endgroup$
  • 1
    $\begingroup$ Thanks Matija! How do you get away with not having this rule? How could you apply the state handler (when it's not inline) to a computation that has more effects than just lookup and update? I guess you would have to inline all handlers? $\endgroup$ – Labbekak May 7 '18 at 14:44
  • 1
    $\begingroup$ You can get away by let-polymorphism (which is not included in the paper you linked) and assign the type $\forall A, B, \Delta. \; B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \Delta) ! \Delta$ to the handler. See our latest ESOP paper on this topic. $\endgroup$ – Matija Pretnar May 8 '18 at 3:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.