# Question on subtyping of handlers in “An Effect System for Algebraic Effects and Handlers”

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.

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.
• 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. – Matija Pretnar May 8 '18 at 3:32