Question on subtyping of handlers in "An Effect System for Algebraic Effects and Handlers"

Question

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.

Answer 1

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.