# Composition of handler types in algebraic effects and handlers

In the paper "An introduction to algebraic effects and handlers" (Pretnar, Matija. Electronic Notes in Theoretical Computer Science 319 (2015): 19-35), handlers get a handler type that looks like a function type: $\underline{C} \Rightarrow \underline{D}$. These can be "applied" with the with h handle c syntax.

What I've noticed is that the only way to get a handler type is with the handler syntax, which means there's no way to get composition of handler types: given $\underline{A} \Rightarrow \underline{B}$ and $\underline{B} \Rightarrow \underline{C}$ there is no way to get $\underline{A} \Rightarrow \underline{C}$.

I believe this is because there is no abstraction for computations like there is an abstraction for values ($\lambda x . c$). Is this left out because of simplicity of is there a problem with such abstractions which means you can never have composition of handler types in a consistent system?

You are correct that the reason lies in the lack of computation abstractions. They are left out because they are not a standard programming construct, especially in a call-by-value calculus. But even if you added them, I don't think they should be given a type of the form $\underline X \Rightarrow \underline Y$ because they are in general not homomorphisms, what the type would suggest.

You can get around in two ways:

1. you can apply the function fun t -> with h' handle (with h handle t ()) of type $(\mathtt{unit} \to \underline A) \to \underline C$ on a thunked operation. For example, in Multicore OCaml the only way of making a general handler is through a function that takes a thunked computation.

2. you can precompose the handler similar to what @chi suggested. If h is of the form

handler {
return x -> c_ret,
op1(x, k) -> c1(x, k),
...
}


then the composed handler

handler {
return x -> with h' handle c_ret,
op1(x, k) -> with h' handle c1(x, k),
...
}


has the type $\underline A \Rightarrow \underline C$.

• Thanks Matija! I believe Koka does something like (1), there are no handler types there. Do you feel like handler types are essential? The way Andrej Bauer told it, they were nice for the theoretical background. Maybe handlers could be given the time $(T \rightarrow \underline A) \rightarrow (T \rightarrow \underline B)$, now handler application and types can be removed. Do you think this is a bad idea? Feb 6 '18 at 9:05
• I just realized in that case the $\rightarrow$ denotes both functions and handlers, two different types of values. Which is probably not a good idea. Feb 6 '18 at 10:54

I only had a cursory look to the paper, but I think that, if $h: \underline A \Rightarrow \underline B$ and $h': \underline B \Rightarrow \underline C$, then

handler
{ return x -> with h' handle (with h handle (return x))
, op1(x,k) -> with h' handle (with h handle (op1(x,k)))
, ...
}


has the wanted type $\underline A \Rightarrow \underline C$.

• No, there is a mistake in the case for op1 (and other operations). If the composed handler had the type $\underline A \Rightarrow \underline C$, the type of the continuation would be $A_{op} \to \underline C$ because handlers continue to handle the continuation. Therefore, the computation op1(x,k) on the right hand side would have the type $\underline C$, which doesn't match $\underline A$ that the handler h expects. Feb 6 '18 at 5:25
• It would work for shallow handlers though (ones that handle only the first instance of the operation and don't implicitly resume handling the continuation) Feb 6 '18 at 5:59