Poly-morphic effect handlers

Abstract

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.

Example

A program may display data using the PRINT effect:

PRINT("Training model...")
model = train_model(training_data)
PRINT("Evaluating accuracy...")
accuracy = test_model(model, testing_data)
PRINT("Accuracy: " + accuracy)
return model

This program displays information about its current status as it executes. The program uses the PRINT effect, which we describe mathematically using the following effect signature: \begin{aligned} \mathsf{print}[s] &: 1 \end{aligned} Here, s : S refers to an arbitrary string. The result type 1 indicates that printing does not compute any interesting data.

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

Example

As another example, the following pseudocode implements a simple password authenticator based on mutable state:

guess = READ()  # read the guess from memory
if guess == "polynomial":
    WRITE("")  # overwrite the correct guess
    return True
else:
    return False

This program has type 2 (i.e., a Boolean), computing either True or False. First, it performs the READ effect to take the password guess out of memory. If the guess was correct, it overwrites the guess with the empty string and returns True; otherwise, it simply returns False. The program involves two effects: \begin{aligned} \mathsf{read} &: S \\ \mathsf{write}[s] &: 1 \end{aligned} The \mathsf{read} effect returns a string of type S; the write-to-memory effect is similar to \mathsf{print} from before.

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

Example

When a programmer attempts to divide by zero, the program should produce an error. The following pseudocode for divide(numerator, denominator) implements this behavior:

if denominator == 0:
    ERROR()
else:
    return numerator / denominator

This program uses the following effect signature: \begin{aligned} \mathsf{error} &: 0 \end{aligned} The result of \mathsf{error} is an element of the empty type, which is impossible to construct. In other words, no code follows an error being signaled.

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

Example

The following pattern is commonly used to recover after an error has been encountered:

try:
    return divide(a, b)
handle:
    ERROR() => return 0  # if ERROR() caused, instead just return 0

This takes the program divide(a, b) that may produce an error and turns it into a program that does not involve effects.

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

Example

Printing can be handled to augment the printed strings.

handle:
    PRINT(s) => PRINT(capitalize(s))

Every time the programmer used the PRINT(s) effect, we instead print s in all capital letters.

Example

Printing can be implemented in terms of mutable state:

handle:
    PRINT(new_string) =>
        old_strings = READ()
        WRITE(old_strings + new_string)

In order to implement the PRINT effect, one can read the data already printed from memory and write the same strings back with the new string appended. This handler takes a program that may use PRINT and turns it into a program that may use READ and WRITE.

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.

Example

The effect signature \begin{aligned} \mathsf{print}[s] &: 1 \end{aligned} corresponds to polynomial Sy^1 = Sy. The effect signature \begin{aligned} \mathsf{error} &: 0 \end{aligned} corresponds to polynomial y^0 = 1.

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})}

Example

The effect signature \begin{aligned} \mathsf{read} &: S \\ \mathsf{write}[s] &: 1 \end{aligned} corresponds to polynomial y^S + Sy.

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

Definition

Let p be a polynomial. A p-algebra consists of a set A along with an algebra map \alpha : p \triangleleft A \to A.

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

Example

Consider the polynomial Sy corresponding to the printing effect. A Sy-algebra is a set A equipped with a map \mathsf{print} : S \times A \to A, or equivalently a monoid action of the free monoid on generators S.

Remark

In general, when p is a coproduct, an algebra map can be constructed out of algebra maps for each components using the universal property. For example, an algebra map for p = y^S + Sy consists of two maps: \begin{aligned} \mathsf{read} &: A^S \to A \\ \mathsf{write} &: S \times A \to A \end{aligned}

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

Definition

Let p be a polynomial functor. The category \mathbf{Alg}({p}) has objects p-algebras. A morphism (A, \alpha : p \triangleleft A \to A) \to (B, \beta : p \triangleleft B \to B) consists of a map f : A \to B such that \alpha \mathbin{;} f = (p \triangleleft f) \mathbin{;} \beta.

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

Example

When p = Sy, a morphism (A, \mathsf{print}_A : S \times A \to A) \to (B, \mathsf{print}_B : S \times B \to B) is a map f : A \to B such that for all a : A, f(\mathsf{print}_A(s, a)) = \mathsf{print}_B(s, f(a))

Example

When p = 0, an algebra map 0 \triangleleft A \cong 0 \to A is trivial. Therefore, \mathbf{Alg}({0}) is equivalent to \mathbf{Set}, containing only pure¹ programs.

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”² of p-effects.

Definition

The free monad on p, written \mathfrak{m}_{p}, is the polynomial functor that is the least fixed point to the following isomorphism: \mathfrak{m}_{p} \cong y + p \triangleleft \mathfrak{m}_{p} This polynomial \mathfrak{m}_{p} forms a monad in \mathbf{Poly}, along with maps \begin{aligned} y &\to \mathfrak{m}_{p} \\ \mathfrak{m}_{p} \triangleleft \mathfrak{m}_{p} &\to \mathfrak{m}_{p} \end{aligned} to construct pure computations and concatenate two sequences of effects, respectively. More description is given in David’s recent blog post.

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

Definition

The free p-algebra functor, F_p : \mathbf{Set}\to \mathbf{Alg}({p}), sends a set X to the algebra with underlying set \mathfrak{m}_{p} \triangleleft X. The corresponding algebra map is defined using the following right coproduct injection map: p \triangleleft \mathfrak{m}_{p} \to y + p \triangleleft \mathfrak{m}_{p} \cong \mathfrak{m}_{p} Then, the algebra map p \triangleleft \mathfrak{m}_{p} \triangleleft X \to \mathfrak{m}_{p} \triangleleft X is the lift of this map via (-) \triangleleft X.

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.

Example

If p = Sy, then \mathfrak{m}_{p} \triangleleft X is isomorphic to S^\star \times X, a list of printed strings and a result of type X. The algebra map \mathsf{print} : S \times (S^\star \times X) \to S^\star \times X prepends the given string to the list.

Example

If p = 1, then \mathfrak{m}_{p} \triangleleft X is isomorphic to X + 1; this is the error monad applied to X. The algebra map \mathsf{error} : 1 \to X + 1 is simply the right injection, identifying the data in the underlying set representing an error.

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.

Remark

The category \mathbf{Alg}({p}) is monadic over \mathbf{Set}, where the monad is \mathfrak{m}_{p}.

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:

1. a polynomial p : \mathbf{Poly} describing the effects available, and
2. 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).

Example

The polynomial 1 represents a single error effect. A handler on a free algebra, (1, F_1 X) \leadsto (q, (B, \beta)), consists of the following:

• A 1-algebra structure \beta' : 1 \triangleleft B \to B. Since 1 \triangleleft B \cong 1, this is simply \beta' : 1 \to B, an element of B.
• A morphism F_1 X \to (B, \beta'). Since F_1 is a left adjoint to U_1, this is equivalent to a \mathbf{Set} morphism X \to B.

As desired, then, an error handler consists of a designated element of the output type B (in case of an error) and a function X \to B.

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.

Issue

Consider the proposed composition (p, (A, \alpha)) \leadsto (q, (B, \beta)) \leadsto (r, (C, \gamma)). The first handler includes maps \begin{aligned} \beta' &: p \triangleleft B \to B \\ f &: (A, \alpha) \to (B, \beta') \end{aligned} and the second includes maps \begin{aligned} \gamma' &: q \triangleleft C \to C \\ g &: (B, \beta) \to (C, \gamma'). \end{aligned} How would one construct the requisite map p \triangleleft C \to C incorporating p-effects into C?

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.

Example

Let p = q = Sy, representing printing. Then, a morphism p \to q is equivalent to a \mathbf{Set}-map S \to S. Such a polymorphic effect handler could alter strings arbitrarily; for example, as in the introduction, a handler could capitalize every printed character.

Non-Example

Let q = 0, meaning that no effects are present. Then, unless p = 0 too, there are no morphisms p \to q. In particular, if p = 1, representing the ability to error, one may not handle the p-effect of erroring as a non-existent q-effect. Since this morphism must be defined polymorphically, it is no longer legal to choose a designated element of the underlying set of the codomain; now, effect handlers exist “prior to” types.

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

Definition

The category of simple polymorphic effect handlers is defined as follows:

• An object (p, (A, \alpha)) consists of an effect signature p : \mathbf{Poly} and a p-algebra (A, \alpha), as before.
• A morphism (p, (A, \alpha)) \to (q, (B, \beta)) consists of two components:
  1. A handler component \varphi : p \to q in \mathbf{Poly}, translating p-effects into q-effects.
  2. A data component (A, \alpha) \to (B, \beta') in \mathbf{Alg}({p}), which is a \mathbf{Set}-map A \to B that respects the algebra maps \alpha and \beta', where \beta' : p \triangleleft B \to B is the following composite:

  

  In other words, \beta' incorporates a p-effect into B by first translating it to a q-effect and then incorporating the q-effect using the given algebra map \beta.

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.

Definition

A morphism (p, (A, \alpha)) \to (p, (B, \beta)) is called vertical when its handler component is trivial, i.e. \varphi = \text{id}_p. Such a morphism only consists of a morphism (A, \alpha) \to (B, \beta) in \mathbf{Alg}({p}), as we considered before handlers were introduced.

In effect-speak, we might call a vertical morphism a p-effectful program, a program that only addresses data (possibly by performing p-effects) without handling any effects.

Definition

A morphism (p, (A, \alpha)) \to (q, (A', \alpha')) is called cartesian when its data component is trivial. Formally, this means that both A \cong A' and \alpha is the following composite:

In other words, (A, \alpha) and (A', \alpha') are equivalent up to the handler component \varphi.

In effect-speak, we might call a horizontal morphism a polymorphic effect handler from p to q, a program that only handles effects without altering data otherwise.

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

Theorem

Every morphism in \int^\mathbf{Poly}\mathbf{Alg}({-}) factors as a vertical morphism followed by a horizontal one.

In other words, every morphism (p, (A, \alpha)) \to (q, (B, \beta)) can be rewritten as a p-effectful program followed by a polymorphic effect handler from p to q.

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}!

Lemma

The assignment p \mapsto \mathfrak{m}_{p} forms a monad on \mathbf{Poly}, along with maps \begin{aligned} p &\to \mathfrak{m}_{p} \\ \mathfrak{m}_{\mathfrak{m}_{p}} &\to \mathfrak{m}_{p} \end{aligned} that are natural in p. Note that these are similar to the singleton and concatenation maps of the list (free monoid) monad; the former takes a single p-effect and treats it like a singleton sequence of effects, and the latter takes a sequence of sequences of p-effects and flattens it out.

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

Example

Let p = q = Sy, representing printing. In {\mathbf{Poly}}_{\mathfrak{m}_{}}, a map p \to q is equivalent to a \mathbf{Poly}-map Sy \to \mathfrak{m}_{Sy}, which is equivalent to a \mathbf{Set}-map S \to S^\star. So, each time a string printing effect is performed, it may be replaced by a finite-length list of new strings to print.

Example

In the introduction, we considered handling printing as a read-write sequence. Let p = Sy to represent printing, and let q = \{\mathsf{read}\}y^S + \{\mathsf{write}\}Sy to represent reading and writing from a global state storing a string. To handle printing as a read followed by a write, we give a map p \to q in {\mathbf{Poly}}_{\mathfrak{m}_{}}. It suffices to give a map on positions, specified as follows: s \mapsto \mathsf{read}(s' \mapsto \mathsf{write}[s' \cdot s](\mathsf{return})) Since Sy only has a single direction, the map on directions is trivial.

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

Bauer, Andrej. 2018. “What Is Algebraic about Algebraic Effects and Handlers?” arXiv. https://doi.org/10.48550/arXiv.1807.05923.

Bauer, Andrej, and Matija Pretnar. 2014. “An Effect System for Algebraic Effects and Handlers.” Logical Methods in Computer Science Volume 10, Issue 4 (December). https://doi.org/10.2168/LMCS-10(4:9)2014.

Myers, David Jaz. 2021. “Cartesian Factorization Systems and Grothendieck Fibrations.” arXiv. http://arxiv.org/abs/2006.14022.

Plotkin, Gordon D., and Matija Pretnar. 2013. “Handling Algebraic Effects.” Logical Methods in Computer Science Volume 9, Issue 4 (December). https://doi.org/10.2168/LMCS-9(4:23)2013.

Plotkin, Gordon, and Matija Pretnar. 2009. “Handlers of Algebraic Effects.” In 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

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

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

3. See Myers (2021) for an expository account.