We describe Cartwright and Felleisen's modular and compositional approach to effects, discuss extensions and present its implementations in Haskell. The principal ideas, in the words of Cartwright and Felleisen, are:
When designing a program we should start thinking what effect we want
to achieve rather than which monad transformer to use. Instead of
jumping straight to
StateT and so on, we ought to identify what
transformation on the world and its resources we wish to
effect. Written formally, this transformation often takes the form of an
effect handler. Our framework is designed around such handlers,
encouraging custom effects for program fragments and their composition.
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.
Joint work with Amr Sabry and Cameron Swords.
The annotated slides of the talk presented at the Haskell Symposium 2013 on September 23, 2013 in Boston.
An implementation of extensible effects
Eff.hs (importing an implementation of open unions)
defines and implements the API for extensible effects. It also
implements the standard monadic effects such as exception, state, and
non-determinism. The file contains many examples and test code.
This particular implementation of extensible effects is based on the composition of codensity and free monads. There are other implementations, involving neither codensity nor free monads.
Defining a new class for each effect, such as
is possible but not needed at all. With monad transformers, a
class per effect is meant to hide the
ordering of transformer layers in a monad transformer stack. Effect
libraries abstract over the implementation details out of the
box. Crutches -- extra classes -- become unnecessary.
The warm-up example: the single
Reader effect as an interaction with an authority. This is the code for Sec 3.1 of the paper.
Reader00.hs describes the single
Reader Int effect; the other file generalizes to arbitrarily typed environment monad.
A variation of
Eff.hs emulating monad transformer classes of MTL.
The framework of extensible effects indeed can define the instances
MonadState, etc. These instances
require fewer annotations in the user code; on the other hand, they
are less general, enforcing a single effect layer of a particular kind.
A few micro-benchmarks
Monad transformers have become an integral part of Haskell, with many tutorials. Rarely do the drawbacks of transformers get a mention. As a rare exception, Chapter 18 of `Real World Haskell' points out the overhead added by each monad transformer layer, an occasional need for the ungainly explicit lifting, and the difficulty of building monad transformer libraries: when adding a new transformer, one has to explicitly specify `lifting', its interaction with all other transformers. Alas, the biggest drawback of monad transformers is hardly mentioned at all.
Monad transformers have an inherent limitation: they enforce the static ordering of effect layers and hence statically fixed effect interactions. There are practically significant computations that require interleaving of effects and that cannot therefore be implemented with monad transformers. `Delimited Dynamic Binding' (ICFP 2006) was first to bring up this point. The `Extensible Effects' paper expanded that discussion on new examples. Section 5 describes simple and common programming patterns that cannot be efficiently, or even at all, implemented with monad transformers because the static ordering of effect layers is not flexible.
Bryan O'Sullivan, Don Stewart, and John Goerzen: Real World Haskell
Chapter 18. Monad transformers
< http://book.realworldhaskell.org/read/monad-transformers.html#id6594 >
An early compelling case for open unions are extensible exceptions,
which have been part of Haskell for
many years (Simon Marlow, Haskell Workshop 2006). To permit throwing
exceptions of arbitrarily many types, the thrown exception value is an
open union (see
Control.Exception). Raising an
exception puts -- injects -- a particular exception value into the open
union. When we handle an exception, we project: check if the
thrown exception is of a particular desired type. (Extensible
effects operate in the same manner; a request for an effect
also has a return address to resume
the computation.) Thus, at its core, an open union should let us inject a value of any type into the union and to project a type
from the union, that is, to find find out if the value in
the union has a given type.
The open-union type of exceptions,
SomeException (or the similar
exn in ML), gives no indication of possible summands -- that is,
which particular exception types may be in the union. Therefore,
neither Haskell nor ML can ensure that a program handles all
exceptions that could be raised during its execution.
To do better, the type of an open union should be annotated with the set of possible summands. The injection function will add the type
of the injected value to the union type, unless it was there already.
As always with types, the type of the open union is an approximation
for the type of the value therein. Consider the
Either Int Bool: at run time, the union value is
either a single
Int or a single
Bool. The union type is an
approximation: we cannot generally determine at compile-time the
Bool, of the value stored in the union. We
are sure however that this type is not a
String and hence attempting
to project a
String value from an
Either Int Bool union is a
compile-time error. Such type-annotated union is called a type-indexed
The familiar data type
(Either a b) is the simplest example of typed
unions, but it is not extensible. The
Right are injections, and the projections
are realized via pattern-matching:
prj1:: Either a b -> Maybe a prj1 (Left x) = Just x prj1 _ = NothingThe type checker does not let us inject a value of a type other than
Either a b, hence restricting injection to values that participate in the union. We can only project at types
Either a bis a union of exactly two types, and thus not extensible. Furthermore, it is not abstract: we must know the exact structure of the union in order to choose the proper injection,
Right. The type
Either Int Boolis different from
Either Bool Int, although they are morally the same union.
Heeding the drawbacks of
Either, we arrive at the following
interface for open unions:
data Union (r :: [*]) -- abstract type family Member (t :: *) (r :: [*]) :: Constraint inj :: Member t r => t -> Union r prj :: Member t r => Union r -> Maybe t decomp :: Union (t ': r) -> Either (Union r) t
The union type
Union r is tagged with
r, which is meant to be a
set of summands. For the lack of type-level set,
it is realized as a type-level list, of the kind
[*]. The injection
inj and the projection
prj ensure that the type
t to inject
or project must be a member of the set
r, as determined by the type-level
Member t r. The function
decomp performs the orthogonal
decomposition. It checks to see if the union value given as the
argument is a value of type
t. If so, the value is returned as
Right t. Otherwise, we learn that the received union value does
not in fact contain the value of type
t. We return the union,
adjusting its type so that it no longer has
t. The function
decomp thus decomposes the open union into two orthogonal ``spaces:''
one with the type
t and the other without. The decomposition operation,
which shrinks the type of open unions, is the crucial distinction
of our interface from the previous designs (Liang et al. 1995,
Swierstra 2008, polymorphic variants of OCaml). It is this decomposition
operation, used to `subtract' handled exceptions/effects, that
insures that all effects are handled. The constraint
Member t r
may be seen as the interface between
prj on one hand
decomp on the other hand: for each injection or projection
t there shall be a
decomp operation for the type
This basic interface of open unions has several variations and
implementations. In extensible effects, the summands of the open
union have the kind
* -> * rather than
*. One implementation,
described in the extensible effects paper, takes open unions to be
Dynamic. Therefore, all operations on open unions take constant time.
This is the second distinction of our open unions from those by
Liang et al. 1995 and Swierstra 2008. (Polymorphic variants in OCaml
also have constant-time operations). The extensible effects
implementation is essentially the one described in the full HList
paper, Appendix C, published in 2004.
One may notice a bit of asymmetry in the above interface. The functions
prj treat the open union index
r truly as a set of types.
The operations assert that the type
t to inject or project is a member
of the set, without prescribing where exactly
t is to occur in the concrete
r. On the other hand,
decomp specifies that the type
t must be at the head of the list that represents the set of summand
types. It is unsatisfactory, although has not presented a problem
so far for extensible effects. If the problem does arise, it may
be cured with an easily-defined conversion function of the type
conv :: SameSet r r' => Union r -> Union r', akin to an annotation.
The other solutions to the problem (based on constraint kinds, for example)
are much more heavier-weight, requiring many more annotations. Perhaps
implicit parameters may help:
e1 = if ?x then ?y else (0::Int) -- inferred: e1 :: (?x::Bool, ?y::Int) => Int f :: ((?x::Bool) => r) -> r -- explicit signature required f x = let ?x = True in x t1 = f e1 -- inferred: t1 :: (?y::Int) => IntThe inferred type of
t1no longer contains the
?x::Boolconstraint, which thus has been subtracted. The type of the `subtraction function'
f, the handler, only mentions the removed constraint, saying nothing of other constraints or if there are other constraints. Binding an implicit parameter builds the dictionary and makes the constraint go away. One could wish the same for proper constraints.
One may notice that the open union interface, specifically,
decomp, does not check for
duplicates in the set of summands
r. This check is trivially to add --
in fact, the HList implementation of type-indexed co-products did
have such a check and so implemented true rather than disjoint unions.
In case of extensible effects, the duplicates are harmless, letting us
nest effect handlers of the same type. The dynamically closest
handler wins -- which seems appropriate: think of reset in delimited
control. There is even a test case for nested handlers in
Discussions of extensible effects tend to derail to an insignificant
side-issue of one particular implementation of open unions,
OpenUnion1. That implementation relies on
Dynamic (that is,
Typeable) and uses
OverlappingInstances to implement
Member. It should be stressed that neither of these features are
essential and there are other implementations of open unions without
OpenUnion1, the overlapping instances are enabled only within that
module. The rest of the user program does not need the extension. The
extension is used to implement a closed class
Member, which is not meant to be user-extensible. In fact, the type
class emulates closed type families, which are coming GHC. With the
closed type families, no overlapping instances are needed.
We have thus seen the design space for typed open unions and a few sample implementations. Hopefully more experience will help choose an optimal implementation and introduce it into Haskell.
Another, somewhat dual implementation, relying on universals rather than existentials
The old implementation of open unions, without overlapping instances or Typeable
The first modern implementation of extensible effects (February 2012). The first two files are the warm-up examples, leading to the full implementation.
Cartwright and Felleisen's paper appeared just a bit prior to Liang, Hudak and Jones' ``Monad Transformers and Modular interpreters'' that introduced monad transformers. In fact, the monad transformers paper mentions Cartwright and Felleisen's direct approach in footnote 1. Perhaps because Cartwright and Felleisen demonstrate their approach in an obscure dialect of Scheme, their work did not receive nearly as much attention as it vastly deserves.
We implement the enhanced EDLS in Haskell and add delimited control. To be precise, we implement the Base interpreter (whose sole operations are Loop and Error) and the following extensions: CBV lambda-calculus, Arithmetic, Storage, Control. The extensions can be added to the Base interpreter in any order and in any combination.
Our implementation has the following advantages over EDLS:
Our main departure from EDLS is is the removal of the `central authority'. There is no semantic `admin' function. Rather, admin is part of the source language and can be used at any place in the code. The `central authority' of EDLS must be an extensible function, requiring meta-language facilities to implement (such as quite non-standard Scheme modules). We do not have central authority. Rather, we have bureaucracy: each specific effect handler interprets its own effects as it can, throwing the rest `upstairs' for higher-level bureaucrats to deal with. Extensibility arises automatically.
We take the meaning of a program to be the union of Values and (unfulfilled) Actions. If the meaning of the program is a (non-bottom) value, the program is terminating. If the meaning of the program is an Action -- the program finished with an error, such as an action to access a non-existing storage cell, or shift without reset, or a user-raised error.
EDLS says, at the very top of p. 3, that the handle in the effect message ``is roughly a conventional continuation.'' Because the admin of EDLS is `outside' of the program (at the point of infinity, so to speak), its continuation indeed appears undelimited. By making our `admin' part of the source language, we recognize the handle in the effect message for what it is: a delimited continuation.
The complete code in Haskell98 (plus pattern guards), including several examples.
This code is not written in idiomatic Haskell and does not take advantage of types at all. The ubiquitous projections from the universal domain tantamount to ``dynamic typing.'' The code is intentionally written to be close to the EDLS paper, emphasizing denotational semantics, whose domains are untyped. One can certainly do better, for example, employ user-defined datatypes for tagged values, avoiding the ugly string-tagged values.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML