Home

Handlers of Algebraic Effects

Matija Pretnar, Gordon Plotkin (2009) Handlers of Algebraic Effects:

We present an algebraic treatment of exception handlers and,
more generally, introduce handlers for other computational effects repre-
sentable by an algebraic theory. These include nondeterminism, interac-
tive input/output, concurrency, state, time, and their combinations; in
all cases the computation monad is the free-model monad of the theory.
Each such handler corresponds to a model of the theory for the effects
at hand. The handling construct, which applies a handler to a compu-
tation, is based on the one introduced by Benton and Kennedy, and is
interpreted using the homomorphism induced by the universal property
of the free model. This general construct can be used to describe previ-
ously unrelated concepts from both theory and practice.

Handling a computational effect, such as raising an exception, amounts to homomorphically mapping the handled computation onto another computation. So, for example, raise is interpreted as the exception handling code given to the handler.

While encompassing both returning and non-returning handlers, this idea becomes more interesting when you start to handle the other effects, such as lookup and update. Then you can get things like state rollback when an exception occurs, and others (CSS renaming and hiding, stream redirection, timeout). Thus the semantics of handlers gives rise to a new programming construct.

If you want a gentler introduction to the subject (along with Plotkin's algebraic theory of effects and Levy's Call-by-Push-Value), try Pretnar's 2010 thesis.

By Ohad Kammar at 2010-07-04 09:54 | Semantics | other blogs | 13300 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The spectrum of computational effects: two questions

This work seems to follow from the work of Plotkin & Power, 2001, Notions of computation determine monads. Where does this line of work lie on the spectrum from Lawvere theories (Hyland & Power, cf. Lawvere theories and monads) to the full generality of monads? Does use of the term "algebraic effects" mean that we are talking about something more restrictive than "computational effects"?

I wish I would make the time to understand this field properly. I've got the impression that some people are going to do very cool things with this stuff.

By Charles Stewart at Tue, 2010-07-06 14:09 | login or register to post comments

Two answers

Where does this line of work lie [..] to the full generality of monads?

This question is under investigation at the moment (by myself, by Pretnar --- anyone else?). My intuition is that it is. However, due to the opaque nature of monads, there is a lot less you can do with monads in general. So, certainly in terms of semantics, you can have "monad handlers".

Does use of the term "algebraic effects" mean that we are talking about something more restrictive than "computational effects"?

The answer is a recurring theme with the algebraic theory of effects: The more algebraic the monad, the more structure you can get for free about the semantics, and the more you can talk (in general terms) about the semantics. In this case, you get a syntactic structure (effect handlers) for handling the effects arising inside that algebraic theory. In this case, the main problem with monads is that the effect operations are separate from the monad, so handling them in general is trickier. If you can manually define ad-hoc syntactic+semantics forms to handle the effects of the monad, you would get a handler for a non-algebraic monad.

Did I answer your questions?

I wish I would make the time to understand this field properly. I've got the impression that some people are going to do very cool things with this stuff.

I agree. As I wrote earlier, Pretnar's thesis has a gradual introduction to the topic. You can start there before delving into the denser papers.

By Ohad Kammar at Tue, 2010-07-06 15:48 | login or register to post comments

Thanks

Did I answer your questions?

Yes, and you've convinced me to put Pretnar's dissertation on my list of to-reads. I'll report back when I have got further with that.

By Charles Stewart at Wed, 2010-07-07 08:17 | login or register to post comments