<p>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).</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 4.0
2018-05-07T14:44:02.050Z
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?
Labbekak
CC BY-SA 4.0
2018-05-08T03:32:25.237Z
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](https://people.cs.kuleuven.be/~tom.schrijvers/portfolio/esop2018.html) on this topic.
Matija Pretnar
CC BY-SA 4.0
2018-05-07T06:47:54.133Z
2018-05-07T06:47:54.133Z
Matija Pretnar
<p>I had a question on subtyping in the paper <a href="https://arxiv.org/pdf/1306.6316.pdf" rel="noreferrer">"An Effect System for Algebraic Effects and Handlers"</a>. I was wondering why there isn't a subtyping rule for adding effects on both sides of a handler type, something like this:</p>

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

<p>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.</p>

<p>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.</p>

<pl.programming-languages>
Question on subtyping of handlers in "An Effect System for Algebraic Effects and Handlers"
Labbekak
# Question on subtyping of handlers in "An Effect System for Algebraic Effects and Handlers"

(Asked by: username_0 on 2018-05-06)

I had a question on subtyping in the paper ["An Effect System for Algebraic Effects and Handlers"](https://arxiv.org/pdf/1306.6316.pdf). 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.

**Tags:** pl.programming-languages

---

## 1 answers

### Answer by username_1 on 2018-05-07. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_1**: 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](https://people.cs.kuleuven.be/~tom.schrijvers/portfolio/esop2018.html) on this topic.  

---

