Algebraic effects and handlers at OPLSS 2018

I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:

I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming language out of them, and how to program with handlers.

Rafael Castro

Nice to see that the lectures were recorded!

Regarding (2), in Haskell one often has the problem of "combining" monads, which has no general solution; algebraic effects seem to solve this. Is the algebraic "monad coproduct" approach at all related to Haskell's "monad transformers" that allow certain monads to be combined with any other monad?

Regarding (3), I am a little puzzled by the notion of handler from a mathematical perspective. It seems to me that the mathematically natural way to talk about a homomorphism from F_T(X) to F_{T'}(X') would be to ask for a monad morphism from T to T', thereby making every T'-model into a T-model functorially, and then a T-homomorphism from F_T(X) to F_{T'}(X') (hence a set-map from X to F_{T'}(X')). Syntactically, I think this means that the operation handlers would not be allowed to know or use the "return type" of the with-handle expression, instead being forced to return a value constructed in a generic way from the supplied continuation. Of course this would rule out basic things like exception handlers (Example 3.1), so it's not as useful. But can you give any more mathematical intuition for the notion of handler?

Regarding (2): yes, the fact that algebraic effects can be combined more easily is often considered to be an advantage over monads.

Regarding (3): you're right, with your notion of handler the handlers would have to be generic in the return values. Man handlers are like that (sate, I/O), but some important ones are not, for instance, a handler which handles non-deterministic choice and computes the maximum possible return value relies on the fact that return values can be compared. I think handlers arise as a combination of two requirements: we want to use free algebras to model computations, and we want handlers to be algebra homomorphisms. Assuming these requirements, we have several options. Of these, the one presented is the one that programmers seem to be most happy with. This is an empirical observation. (In fact, some programers want "shallow" handlers which correspond to maps between carriers, ignoring algebra structures). I know this is not much of a mathematical explanation, but you are threading into computer science territory :)

Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.