Extensible Effects -- An Alternative to Monad Transformers

Extensible Effects -- An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:

We design and implement a library that solves the long-standing problem of combining effects without imposing restrictions on their interactions (such as static ordering). Effects arise from interactions between a client and an effect handler (interpreter); interactions may vary throughout the program and dynamically adapt to execution conditions. Existing code that relies on monad transformers may be used with our library with minor changes, gaining efficiency over long monad stacks. In addition, our library has greater expressiveness, allowing for practical idioms that are inefficient, cumbersome, or outright impossible with monad transformers.

Our alternative to a monad transformer stack is a single monad, for the coroutine-like communication of a client with its handler. Its type reflects possible requests, i.e., possible effects of a computation. To support arbitrary effects and their combinations, requests are values of an extensible union type, which allows adding and, notably, subtracting summands. Extending and, upon handling, shrinking of the union of possible requests is reflected in its type, yielding a type-and-effect system for Haskell. The library is lightweight, generalizing the extensible exception handling to other effects and accurately tracking them in types.

A follow-up to Oleg's delimited continuation adaptation of Cartwright and Felleisen's work on Extensible Denotational Language Specifications, which is a promising alternative means of composing effects to the standard monad transformers.

This work embeds a user-extensible effect EDSL in Haskell by encoding all effects into a single effect monad using a novel open union type and the continuation monad. The encoding is very similar to recent work on Algebraic Effects and Handlers, and closely resembles a typed client-server interaction ala coroutines. This seems like a nice convergence of the topics covered in the algebraic effects thread and other recent work on effects, and it's more efficient than monad transformers to boot.

Comment viewing options

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

Programming and Reasoning with Algebraic Effects and Dependent T

Reading the abstract, it seems closely related to Programming and Reasoning with Algebraic Effects and Dependent Types by Edwin Brady that will be in ICFP the same week.

Excellent find! They indeed

Excellent find! They indeed look very closely related. This work too uses a type-level list of effects that are equivalent up to permutation (that are provided as proofs), which seems equivalent to the open union approach. Brady's paper seems to say that it can't currently model non-deterministic choice, but "Extensible Effects" paper does provide support for this if I recall correctly, so they are likely not exactly equivalent.

Handlers in action

And a third one, by Kammar, Lindley and Oury, also at ICFP'13:

Handlers in action

Is there anything useful in

Is there anything useful in these papers about managing and making effects more useful, or is it just more about restricting them and making sure they are accounted for during type checking? I'm always blown away about how different the FP, OOP, and systems communities look at this topic.

Handling effects is more than just typing them

A good effect system will give you the power of first class coroutines. Typing effectful systems and being able to capture them first class is a huge advantage over the typical OOP situation where you have to manually copy a big chunk of the object graph to achieve something similar.

I don't get it, you mean

I don't get it, you mean continuations?

Can you elaborate or point me to a more detailed argument somewhere. I'm genuinely interested here as I'm entering the effect game myself (from the OO perspective), but with a focus on re-execution and rollbacks.

A good effects system allows

A good effects system allows you to override effects, to specify how they are handled - potentially in terms of a different or lower level effects model. There is a lot of flexibility here. Some effects systems look much like exception systems - i.e. you have effects handlers just like you have exception handlers. (Though, there is a significant difference that "hierarchical exceptions" make a lot more sense than "hierarchical effects". You won't be 'catching' a top-level effect then just dropping it.)

OO can achieve the same, e.g. using context objects or capabilities rather than ambient authority to handle the effects. But this takes much developer discipline. For some use cases, OO seems too expressive for precise control of effects because an object can encapsulate invocations of other objects, and thereby hide which effects are invoked from the client of the object. (Objects work well if only the creator of the object needs to control effects.)

Effects systems work best if you want something like ambient authority (where you don't need to pass authorities around explicitly) but also want precise control over those authorities, or some ability to compose and layer them.

I've been idly seeking good ways to reconcile object capabilities with effects systems. My best idea involves modeling capabilities in terms of typed tokens that prove entry in an external registry or memory. Invocation of a capability is then a controllable effect, without revealing anything about the capabilities (the tokens might or might not have an eq function). Creation/registration of capabilities is another controllable effect.

what are effects?

It sounds like effects in this context mean more like "exceptions" than say an imperative assignment to shared state. The latter kinds of effects do not really need to be "handled", though they have non-local consequences.

Which operations are part of

Which operations are part of the effects system is up to the language designer. So is the precision with which effects are distinguished. It would take dependent types to be precise down to the level of controlling access to individual variables or files.

There is no singular answer to 'what are effects'. To a Haskell programmer, effects are anything that doesn't fit into a pure function. To a Linear Logic programmer, effects might include 'information effects' such as duplicating or dropping information.

Assignment to a variable can certainly be an effect. The ability to control this effect might not seem useful until you decide that said variable should be stored in a database, or that uses of the variable by a specific subprogram should be logged, etc.

A major advantage of an expressive effects model is that developers might take a subprogram using high-level effects (e.g. canvas operations, like cairo) then implement all the needed operations. Developers can define their own effects models like virtual machines or DSLs.

But a major weakness of most effects models is that they don't really support optimization, e.g. if you have `x++; x+=2; x++` it's unclear that we can rewrite this to `x+=4`. Indeed, depending on how the `++` and `+=` effects are handled (e.g. potentially printing some message), it may be an invalid optimization. I've been wondering how to address this issue (e.g. providing 'effect-classes' with required equational laws, or assumed rewrite rules) but I haven't found a solution that seems verifiable in practice. This lack of support for local reasoning about a program's behavior, for optimization purposes among others, is one of the reasons I've been resistant to effects systems.

Handlers are about...

...making effects programmable. The idea is that you can specify an effect as a signature, and then specify effect handlers to let you *dynamically* choose the implementation of the effect. The reason they're called effect handlers is because of the way you can implement it.

Basically, when a program runs, you can install an effect handler in a dynamic scope, and when it tries to run an effectful operation, it will throw an exception holding the effect's name, arguments, and the continuation, so that the effect handler can do its thing and then resume execution.

So, for example, you can write a program that does stateful things, and then if you decide that you want all write operations to log themselves (say, to support rollback), you can just change the implementation of the handler, without changing any of client code.

IMO, the fact that this works is kind of wild, and the fact that it actually has a beautiful semantic theory behind it is just bonkers.

So let me translate this

So let me translate this into a language I understand:

  • Effects are basically abstract methods while handlers are implementations of those methods.
  • Dispatch of effects to handlers are dynamically scoped.
  • This enables some form of aspect-oriented programming :)

Dynamically scoped procedures are quite interesting, but the problem of type safety is similar to the problem of dynamic binding in general. Hmm...

This description is

This description is essentially correct, hence my description of the fact that it has a relatively simple denotational semantics with a good equational theory as "bonkers". :)

That is quite useful,

That is quite useful, thanks!

Whenever I look at ideas from Haskell, I always have to sort out what is interesting and what is just fighting the type system and to preserve purity. I know I shouldn't look at it this way, but I just don't see the beauty of those fights.

Why does it need the continuation?

I'm supposing this is like Common Lisp condition handlers... why do you even need to give it the continuation? Isn't the effect handler running "on the (current) stack"?

So you can resume it multiple times

One thing you can do is handle an effect like 'choose [1, 2, 3]' by resuming with each of the possible choices.

OK, thanks. Another

OK, thanks. Another question: are effect systems then anything other than a design pattern built on (delimited) continuations?

I'm sure they are equivalent

I'm sure they are equivalent in some sense (and Oleg can show you how to go back and forth), but IMO a good effect-handler system is much nicer to work with than delimited continuations. You have a little computation and the type tells you what kind of signals it raises. Each kind of signal has its own protocol that defines its interaction with the computation environment. When you are handling a signal from a computation, you may decide to suspend that computation and resume it later. It's all very straightforward and doesn't have the same mind-bending quality that continuations usually do.

Edit: And 'I'm sure that...' was a rhetorical device. I don't actually know they're equivalent. Composing effects modeled as delimited continuations doesn't sound like fun.

Delimited continuations are

Delimited continuations are a "universal effect", in that any definable monadic effect can be expressed in terms of them. Andrezj Filinski proved this almost 20 years ago, in his paper Representing Monads. Here, "definable monadic effect" means any monadic effect whose unit and bind operations are definable in a purely functional language. (So state and continuations are both definable.)

So in a certain sense, all side-effects are a design pattern for delimited continuations. But there's a difference between a side-effect, and an effect system!

An effect system describes which side-effects may be visible to clients -- and many uses of side effects are not visible to clients. (For example, memoizing a function uses stateful side-effects, but does not change it's observable behavior.) So one of the most important features of any effect system is its support for effect masking, which is what lets you say, "This piece of code has an effect e, but since it won't be visible to clients, we can pretend it doesn't have that effect."

In other words, the difference between delimited continuations and effect systems is the difference between values and their types.

Good point

The distinction between handling a single effect and handling all effects generically was nagging at me in my response above. Even without the typing & hiding effects aspect, can you compose effects modeled with delimited continuations generally or must you attend to the composition on a case-by-case basis depending on what the particular effects are?

Looking forward to using this

Ever since I saw Johan G. Granström's "A new paradigm for component-based development" posted here last year, I've been designing around the idea of a system which uses an open sum type for effect requests, and which somehow supports type-safe "shrinking of the union of possible requests." This paper could be just what I've been hoping for!

This is probably what my Processes are

I haven't been through deeply yet, but my initial thought is that this looks very similar to my "processes" abstraction that I've mentioned in the past. As I mentioned in a thread on Eff, the main difference between my system and that of Eff seemed to be that my effects are handled via back and forth with the process, whereas Eff used a substitutional scheme that lifted the entire effectful value. I think this back and forth approach will be much easier for programmers to understand than Eff's substitutions, even though they might end up being equivalent in some sense.

A Proof Assistant Prototype Based on Algebraic Effects and Handl

A Proof Assistant Prototype Based on Algebraic Effects and Handlers talk by Andrej Bauer. And if you're interested in learning about homotopy type theory, this is one of many talks you can find here: IAS Univalent Foundations.