patternMinor
Composition of handler types in algebraic effects and handlers
Viewed 0 times
handlerseffectstypesandhandleralgebraiccomposition
Problem
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
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?
$\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?
Solution
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:
-
you can apply the function
-
you can precompose the handler similar to what @chi suggested.
If
then the composed handler
has the type $\underline A \Rightarrow \underline C$.
You can get around in two ways:
-
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.-
you can precompose the handler similar to what @chi suggested.
If
h is of the formhandler {
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$.
Code Snippets
handler {
return x -> c_ret,
op1(x, k) -> c1(x, k),
...
}handler {
return x -> with h' handle c_ret,
op1(x, k) -> with h' handle c1(x, k),
...
}Context
StackExchange Computer Science Q#87746, answer score: 5
Revisions (0)
No revisions yet.