Composition of handler types in algebraic effects and handlers

Question

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?

Answer 1

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$.

Answer 2

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$.