# Poly-morphic effect handlers

In computer science, programmers often perform effects to interact with the surrounding environment. For example, a program may print strings or interact with mutable state. Then, effects may be handled, implemented in terms of other effects. In this post, we reconstruct a categorical semantics for programs with effects, and we isolate a class of composable effect handlers that may be concisely described in the language of polynomial functors, the free monad monad, and the Grothendieck construction.

# 1 Introduction

In many programming languages, developers can use *effects* in the process of computing a result. For example, a program may use an effect to output information beyond its returned result.

Effects may also compute data, taken from the outside world by reading memory or asking a person for input.

Effects can also be used to halt the execution of a program.

Sometimes, one might want to *handle* an effect, causing a computation to replace its invocation.

In more advanced effect systems, other effects can be handled, as well.

In this post, we will investigate how to understand effects and effect handlers “\mathbf{Poly}-theoretically”—using the category of polynomial functors.

# 2 Effect signatures as polynomial functors

Every effect signature can be represented by a polynomial functor: a position i corresponds to an effect operation, and the directions associated with i are the result type of the effect. The effect signature \begin{aligned} \mathsf{op} &: B \end{aligned} corresponds to the polynomial y^B, and the effect signature \begin{aligned} \mathsf{op}[a] &: B \end{aligned} corresponds to the polynomial Ay^B, with A-many operations \mathsf{op}[a] where each has result type B.

Effect signatures may be concatenated, including the operations from each; this corresponds to the coproduct of their corresponding polynomials. The empty signature for effect-free programs corresponds to polynomial 0. In general, the polynomial corresponding to an effect signature is: \sum_{\mathsf{op}} y^{\mathsf{returnType}(\mathsf{op})}

Given an effect signature represented as a polynomial p, we may now describe the semantics of types in a language with p-effects.

Intuitively, a p-algebra is a set equipped with the ability to “absorb” p-effects.

Such p-algebras form a category, where the morphisms are structure-preserving maps.

In other words, the map f must commute with the inclusion of effects into the carrier.

# 3 The free monad

Notice that there is a functor U_p : \mathbf{Alg}({p}) \to \mathbf{Set} sending every algebra (A, \alpha) to its underlying set, A. In fact, this functor has a left adjoint, F_p : \mathbf{Set}\to \mathbf{Alg}({p}), that sends every set A to its corresponding *free p-algebra*. To define this functor, we must first introduce a key idea: the *free monad* on p. Intuitively, the free monad represents a “sequence”^{2} of p-effects.

Using the free monad, we may define the functor F_p that sends a set to its free p-algebra.

The underlying set of F_p(X) consists of sequences of p-effects terminated by a result of type X. The algebra map, then, prepends a p-effect to the beginning of the sequence.

Since F_p \dashv U_p : \mathbf{Alg}({p}) \to \mathbf{Set}, we have that U_p \circ F_p is a monad on \mathbf{Set}; here, it is the free monad \mathfrak{m}_{p} itself.

# 4 Effect handlers

In their seminal work, G. Plotkin and Pretnar (2009) develop a theory of *handlers* for algebraic effects, allowing effects to be implemented by the programmer. We briefly summarize their development as follows. In our semantics from the previous section, an effect signature polynomial p was fixed; then, effects were stored in the carrier of a given p-algebra. Sometimes, though, we may wish to change a p-effectful program into a q-effectful program by implementing p-effects in terms of q-effects.

In order to reconstruct this using \mathbf{Poly}, we may consider pairs (p, (A, \alpha)) consisting of:

- a polynomial p : \mathbf{Poly} describing the effects available, and
- a p-algebra (A, \alpha) consisting of a set along with an algebra map \alpha for incorporating p-effects.

Then, a handler (p, (A, \alpha)) \leadsto (q, (B, \beta)) could consist of

- a p-algebra structure on B: \beta' : p \triangleleft B \to B describing how to translate p-effects into B, and
- a morphism (A, \alpha) \to (B, \beta') in \mathbf{Alg}({p}).

This description recalls via \mathbf{Poly} what a handler typically looks like in the literature (G. Plotkin and Pretnar 2009; G. D. Plotkin and Pretnar 2013; Bauer and Pretnar 2014).

We may hope, then, to form a category where the objects are pairs (p, (A, \alpha)) and morphisms are handlers. Unfortunately, though, handlers in general do not compose.

Notice that the maps \beta' and \gamma' are not enough to form the composite, since they only assign algebras to specific carriers: a p-algebra on the q-algebra B and a q-algebra on the r-algebra C. Instead, what if a handler from p to q assigned a p-algebra structure on *all* q-algebras uniformly? By making this restriction, we isolate a class of well-behaved effect handlers: those that are *polymorphic*.

# 5 Simple Poly-morphic effect handlers

In order to give every q-algebra B with algebra map \beta : q \triangleleft B \to B a p-algebra structure \beta' : p \triangleleft B \to B, it suffices to precompose with a map p \to q in \mathbf{Poly}. Such a map uniformly—in programmer speak, “polymorphically”—translates every p-effect into a corresponding q-effect, without regard for the underlying set B.

Using this idea, we may define a category whose objects are the pairs of the previous section and whose morphisms are polymorphic effect handlers.

This category has a very elegant description: a morphism between pairs just consists of a morphism on the first components and a morphism on the second components (adjusted appropriately by the handler component). You might recognize this category as the Grothendieck construction of the functor \mathbf{Alg}({-}) : \mathbf{Poly}^\text{op} \to \mathbf{Cat} that sends a polynomial p to its category of p-algebras \mathbf{Alg}({p}), written: \int^\mathbf{Poly}\mathbf{Alg}({-}) = \int^{p : \mathbf{Poly}} \mathbf{Alg}({p}) In our category, every morphism has the ability to both handle effects *and* transform program data. Using terminology from the Grothendieck construction, we may classify certain morphisms that only have one of these behaviors.

The Grothendieck construction has many nice properties. For example, we may import the following theorem^{3} about vertical and cartesian morphisms.

For those more familiar with effect handlers, this may provide some intuition about the Grothendieck construction. For those more familiar with the Grothendieck construction, this may provide some intuition about effect handlers.

# 6 Poly-morphic effect handlers

There is still one aspect of these simple polymorphic effect handlers that is unrealistic: when writing a handler p \to q, every effect in signature p maps to exactly one effect in signature q. In reality, though, a p-effect may be implemented via zero, one, two, or more q-effects. For example, handling a printed string could result in dropping the string or printing two strings. Also, as in the introduction, a print effect may be handled as a read effect followed by a write effect. We augment our previous construction slightly to account for this possibility.

In \mathbf{Poly}, a map p \to q sends each p-effect to a single q-effect. To account for a finite-length sequence of q-effects, we wish to instead write a handler as a morphism p \to \mathfrak{m}_{q}, since the free monad on q represents multiple q-effects in sequence. Do such morphisms form a category, though? In fact, they do, because not only is \mathfrak{m}_{q} a monad on \mathbf{Set}, but \mathfrak{m}_{}{} itself is a monad on \mathbf{Poly}!

Since \mathfrak{m}_{}{} : \mathbf{Poly}\to \mathbf{Poly} is a monad, we may consider its Kleisli category {\mathbf{Poly}}_{\mathfrak{m}_{}}. Its objects the same as the objects of \mathbf{Poly}; however, a Kleisli morphism p \to q in {\mathbf{Poly}}_{\mathfrak{m}_{}} is a map p \to \mathfrak{m}_{q} in \mathbf{Poly}.

We may replace \mathbf{Poly} with {\mathbf{Poly}}_{\mathfrak{m}_{}} in our Grothendieck construction. Since the objects of {\mathbf{Poly}}_{\mathfrak{m}_{}} are the same as the objects in \mathbf{Poly}, not much changes; the assignment \mathbf{Alg}({-}) : {\mathbf{Poly}}_{\mathfrak{m}_{}}^\text{op} \to \mathbf{Cat} is functorial. Now, though, handlers have the desired behavior, mapping each single effect to another effectful program (polymorphically). Thus, we call the Grothendieck construction \int^{{\mathbf{Poly}}_{\mathfrak{m}_{}}} \mathbf{Alg}({-}) = \int^{p : {\mathbf{Poly}}_{\mathfrak{m}_{}}} \mathbf{Alg}({p}) the category of *polymorphic effect handlers*.

# 7 Conclusion

Combining five basic building blocks—\mathbf{Poly}, the category of algebras for a polynomial functor, the free monad monad, the Kleisli category of a monad, and the Grothendieck—we were able to compactly describe an important, well-behaved class of effect handlers. Concisely:

The category of effectful programs and polymorphic handlers is the Grothendieck construction of \mathbf{Alg}({-}) : {\mathbf{Poly}}_{\mathfrak{m}_{}}^\text{op} \to \mathbf{Cat}.

We believe that a polymorphic effect handler corresponds to the notion of a “uniformly simple family of closed handlers” presented by G. D. Plotkin and Pretnar (2013). If you know of other references for the style of polymorphic effect handlers we considered here, please let us know!

This post is the result of research that occurred while I was a Summer 2023 Research Associate at the Topos Institute. Thanks especially to David for collaborating with me on this direction of inquiry, and thank you to Dana Scott, Kevin Arlin, Brendan Fong, and everyone at the Topos Institute for a fun and productive summer! –Harrison

## References

*Logical Methods in Computer Science*Volume 10, Issue 4 (December). https://doi.org/10.2168/LMCS-10(4:9)2014.

*Logical Methods in Computer Science*Volume 9, Issue 4 (December). https://doi.org/10.2168/LMCS-9(4:23)2013.

*Programming Languages and Systems*, edited by Giuseppe Castagna, 80–94. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-00590-9_7.

## Footnotes

Sometimes, pure programs are called “effect-polymorphic”, since they make sense regardless of what effect signature is present.↩︎

In case some effects compute nontrivial data, the “sequence” may branch, with multiple “tails” depending on the computed result. Although this looks more like a tree, we use sequence-based terminology for basic intuition.↩︎