previous   next   up   top

Extensible Effects: an alternative to Monad Transformers

 

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:

We extend the approach with effect encapsulation and types. The result is a flexible effect handling framework, which subsumes monad transformers and overcomes their limitations.

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.


 

Introduction

[Abstract]
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, or greatly cumbersome with monad transformers.

Our alternative to a monad transformer stack is the 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.

Version
The current version is September 2013.
References
exteff.pdf [286K]
Extensible Effects: An Alternative to Monad Transformers
The paper published in the Proceedings of the 2013 ACM SIGPLAN symposium on Haskell, pp. 59-70. Boston, MA, USA. September 23-24, 2013.
doi:10.1145/2503778.2503791

talk.pdf [231K]
The annotated slides of the talk presented at the Haskell Symposium 2013 on September 23, 2013 in Boston.

Eff.hs [28K]
Open Unions
An implementation of extensible effects
The file 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 MonadState, 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.

Reader00.hs [3K]
Reader0.hs [4K]
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.

ExtMTL.hs [9K]
A variation of Eff.hs emulating monad transformer classes of MTL. The framework of extensible effects indeed can define the instances for MonadError, MonadReader, 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.

Benchmarks.hs [16K]
A few micro-benchmarks

 

Limitations of Monad Transformers

Monad transformers are strictly less expressive than extensible effects.

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. `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 are particularly problematic with monad transformers because the static ordering of effect layers is not flexible.

References
transf.hs [10K]
Two examples of limited expressivity of monad transformers: the complete code for Sec 5 of the paper.

Bryan O'Sullivan, Don Stewart, and John Goerzen: Real World Haskell
Chapter 18. Monad transformers
< http://book.realworldhaskell.org/read/monad-transformers.html#id6594 >

 

Open Unions

Extensible effects, as well as extensible interpreters (Liang et al. `Monad Transformers and Modular Interpreters' and later Swierstra's `Data types à la carte') all rely on typed open unions, or open type-indexed coproducts. Open unions, by the name of polymorphic variants, are part of OCaml and proved to be a popular feature. One of their uses is again extensible interpreters. It may be high time Haskell supported typed open unions on par with OCaml. We describe the desired interface, its actual and possible implementations, and the overall design space. We use extensible effects as a running example, in part to justify a rarely considered but often crucial function of orthogonal decomposition.

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 SomeException in 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 simplest union 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 specific type 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 co-product.

The familiar data type (Either a b) is the simplest example of typed unions, but it is not extensible. The constructors Left and Right are injections, and the projections are realized via pattern-matching:

     prj1:: Either a b -> Maybe a
     prj1 (Left x) = Just x
     prj1 _        = Nothing
The type checker does not let us inject a value of a type other than a and b into Either a b, hence restricting injection to values that participate in the union. We can only project at types a and b -- Either a b is 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, Left or Right. The type Either Int Bool is 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 sets, 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 function 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 inj and prj on one hand and decomp on the other hand: for each injection or projection at type t there shall be a decomp operation for the type t.

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 inj and 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 representation of 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) => Int
The inferred type of t1 no longer contains the ?x::Bool constraint, 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, the function 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 Eff.hs.

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 Typeable or OverlappingInstances. In fact, OpenUnion2 uses no OverlappingInstances, relying instead on closed type families recently added to GHC.

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.

References
OpenUnion1.hs [3K]
The code for open unions used in the paper. It is close to the implementation in the HList paper. It relies on Typeable, and emulates closed type families using the overlapping instances extension that is limited to that module.

OpenUnion2.hs [3K]
The version of open union without any overlapping instances, directly using closed type families.

OpenUnion3.hs [3K]
Another, somewhat dual implementation, relying on universals rather than existentials

TList.hs [2K]
The old implementation of open unions, without overlapping instances or Typeable

 

Generic crossover, with extensible effects

We present generic crossover -- the interchange of segments between two algebraic data structures. Our surgery library, of cutting a structure at an arbitrary place and grafting new branches, supports many kinds of crossover, e.g., from three parents. The library shows off extensible effects: of defining a new effect (SYB-aware coroutines) and combining it with two standard effects, state and non-determinism.

In genetics, crossover is the interchange of segments between two chromosomes of the same `type' (or, homologous). Genetic algorithms borrow this term to mean the interchange of segments between two structures representing sets of optimization parameters. These data structures are called chromosomes as well, and the parameters, or features, are also called genes. Here is an example with two chromosomes that are lists of integers (which we write in the explicit (::) and [] notation).

     1  ::  2 ::  3  :: []
     10 :: 20 :: []
First we cut each list in two pieces
     1  ::  2 ::  _      and    3 :: []
     10 ::  _            and   20 :: []
where _ represents the hole, which is left at the place of a cut-off branch. Then we swap the branches, grafting the cut-off branch from one list into the hole of the other.
     1  ::  2 ::  20 :: []
     10 ::  3 :: []
The second example
     1  ::  _ ::  3  :: []   and    2
     _ :: 20 :: []           and   10
cuts the leaves: 2 from the first list and the leaf 10 from the second one. The interchange gives
     1  :: 10 ::  3 :: []
     2  :: 20 :: []
Not all cuts produce swappable branches: e.g., the leaf 1 of the first list is not interchangeable with the branch 3::[] of the second because they have incompatible types. What we have just shown is a so-called cut-and splice crossover. Other variations (with the same cut point for both chromosomes, with two cut points, etc.) can also be easily written with our library.

Our code implements the above surgery, of cutting and grafting. First, we write the generic traversal with branch replacement, using the Scrap-your-boilerplate generic programming library (SYB). Next, we differentiate the traversal obtaining the procedure to cut a branch at an arbitrary point. Finally, we add grafting of the swapped branches cut off two data structures, obtaining the crossover. Although the branches must match in type, the types of the whole structures may differ. We need effects: the coroutine effect for differentiating the traversal, and non-determinism for choosing a cut location. We also need state to keep track of the number of cuts made to a structure.

The most interesting part is the traversal and its differentiation. The traversal function of the signature below receives a data structure, and a function that can examine a branch and possibly replace it.

     newtype Updates = Updates Int  -- update count
     traverse :: Member (State Updates) r =>
           (forall a. (Data a) => a -> Eff r a) ->
           (forall a. (Data a) => a -> Eff r a)

In the latter case, that function should increment the update count, shared among the traversals of all branches. The traversal is terminated when the count exceeds a threshold. The traverse itself is a wrapper over SYB's gfoldl, counting updates to branches.

     traverse f = check_done $ \x -> f x >>= check_done traverse_children
      where
      threshold = 1
      check_done go x = get >>= \case
        Updates n | n >= threshold -> return x
        _                          -> go x
      traverse_children = gfoldl traverse_child return
      traverse_child builda x = liftM2 ($) builda (traverse f x)

To differentiate the traversal -- to suspend it at each encountered branch -- we need a coroutine effect. The branches may have different types: for example, the traversal of an integer list comes across branches of the type Int and [Int]. Therefore, a custom coroutine effect is needed, abstracting the type of a branch and ensuring it supports the Data interface.

     data YieldD v = forall a. Data a => YieldD a (Maybe a -> v)
     yieldD :: (Data a, Member (State Updates) r, Member YieldD r) =>
               a -> Eff r a
     yieldD x = send (inj . YieldD x) >>= \case
                 Nothing -> return x
                 Just x  -> modify (\ (Updates n) -> Updates (n+1)) >> return x
The request YieldD sends to its effect handler a value and waits to be resumed with a possibly new value, which becomes the result of yieldD x after incrementing the update count. If the suspension was resumed with no new value, yieldD x just returns x. The request YieldD is easily turned into the description of a structure with a cut branch. A structure of the type a with a hole of the type b is represented as a function Maybe b -> (Eff r (Cut r a)), that waits for a value to fill the hole with and then produces a new Cut:
     data Cut r a = CDone a | Cut (YieldD (Eff r (Cut r a)))

To differentiate traverse we merely apply it to yieldD, obtaining

     traverse_diff :: Data a => a -> Eff r (Cut r (a,Updates))

The next step, cutting a data structure at a random point, is also easy, by non-deterministically choosing one cut point among the many encountered during the whole traversal.

     random_walk :: (Member Choose r, Data a) => a -> Eff r (Cut r (a,Updates))
     random_walk a = traverse_diff a >>= check
       where
         check y@CDone{}            = return y
         check y@(Cut (YieldD x k)) = return y `mplus` (k Nothing >>= check)

Finally, crossover swaps the branches between two data structures cut at non-deterministically chosen points, provided the branches have the suitable type.

     crossover :: (Member Choose r, Data a, Data b) => a -> b -> Eff r (a,b)
     crossover x y = do
       tx <- random_walk x  
       ty <- random_walk y
       case (tx,ty) of
         (Cut (YieldD x kx), Cut (YieldD y ky)) | Just x' <- cast x, Just y' <- cast y -> do
           (xnew,_) <- zip_up =<< kx (Just y')
           (ynew,_) <- zip_up =<< ky (Just x')
           return (xnew,ynew)
         _ -> mzero

As an example, crossing over [1,2,3] with Just 10 produces three possible results: ([10,2,3],Just 1), ([1,10,3],Just 2) and ([1,2,10],Just 3). There are 18 possible ways to crossover [1,2,3] and [10,20], including the two cases described earlier. The code has more examples, including crossover between two trees.

We have presented the library for generic crossover between two arbitrary algebraic data structures. The library is a showcase for extensible effects, demonstrating how easy it is to define a custom effect for a given problem and use it alongside standard effects. We are spared annoying lifting, so typical of monad transformers. Raising and handling of effects is as simple as using side-effectful operations in ML or other impure languages. Unlike ML however, the effects of a function are seen in its type, and the type checker watches that all effects are handled in the end.

Version
The current version is July 2014.
References
Crossover.hs [6K]
The source code of the library with many crossover examples

 

A bit of history

Perhaps a bit of history may help drawing comparisons with related work. Cartwright and Felleisen's paper that put forward extensible denotational language specifications and hence an alternative to monad transformers was presented in April 1994 -- some 8 months ahead of Liang et al. paper on monad transformers. Very unfortunately Cartwright and Felleisen's paper did not receive the attention it deserved and was largely forgotten. I became aware of it in 2004 and found it remarkably inspiring. The translation into Haskell, with the crucial distinction (the authority no longer being central but distributed) was posted on this web site around 2006. A version of extensible effects close to the one described in the Haskell Symposium paper was written in February 2012 and was shown around privately.
References
Extensible interpreters -- an alternative to monad transformers
The early implementation of extensible effects, in a form close to the exposition in the Cartwright and Felleisen's 1994 paper.

Nondet.hs [3K]
Exceptions.hs [2K]
Extensible.hs [12K]
TList.hs [2K]
The first modern implementation of extensible effects (February 2012). The first two files are the warm-up examples, leading to the full implementation.

 

Extensible interpreters -- an alternative to monad transformers

Cartwright and Felleisen have described a technique for composing interpreters that is an alternative to monad transformers. One particular advantage of their technique (hereafter, EDLS) is that the order of composing interpreters, where it is irrelevant, does not have to be specified at all. In fact, unlike monad transformers, we do not have to commit to a single, statically determined order of sub-interpreters. More importantly, object programs are written in the `direct' rather than the monadic (that is, barely hidden continuation-passing) style. Continuation-passing style has many known usability and performance problems. Cartwright and Felleisen's approach also has a theoretical advantage of providing so-called `stable denotations' for expressions (please see their paper for the precise definition). The abstract and page 2 of EDLS paper are particularly insightful.

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.

Version
The current version is 1.5, January 2006.
References
Robert Cartwright, Matthias Felleisen: Extensible Denotational Language Specifications
Symposium on Theoretical Aspects of Computer Software, 1994. LNCS 789, pp. 244-272.
< http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.5941 >

ExtensibleDS.hs [17K]
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.



Last updated July 7, 2014

This site's top page is http://okmij.org/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML