HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Composition of handler types in algebraic effects and handlers

Submitted by: @import:stackexchange-cs··
0
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 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 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 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$.

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.