previous   next   up   top

Extensible Effects vs Data types à la Carte

 

We re-implement Extensible Effects within `Data types à la carte' to demonstrate the difference with the Swierstra's original approach. It turns out that when it comes to effects, Data types à la carte are not extensible or composable. The insight from the Category Theory of evaluation as catamorphism proved misleading.


 

Introduction

One of the most common questions about Extensible Effects is how they compare with Swierstra's famous `Data types à la carte' (hereafter, ALCarte). Similarities are striking: free monads, open unions, `modular' monads leading to a type-and-effect system. Some have wondered if extensible effects are a mere reinvention of ALCarte. This article shows a deep difference between the two approaches: ALCarte lacks encapsulation of effects and, surprisingly, lacks modularity. Introducing a new effect in ALCarte may cause the complete re-implementation of old ones; moreover, each combination of effects may need its own implementation of the whole effect stack. Related to the lack of compositionality are problems with type inference, requiring cumbersome and what should be unnecessary annotations. We conclude with the observation that ideas from the Category Theory may also lead one astray.

The similarities between Extensible Effects and ALCarte are easy to see -- in part because some of them are inevitable. Any extensible (monadic) interpreter has to have, by definition, an extensible type for the terms it interprets. It is no wonder that the extensible union of ALCarte, the (:+:) data type and the (:<:) type class, is essentially the same as the one in the 1995 Liang et al. paper that introduced monad transformers. Some differences between Extensible Effects and ALCarte are also apparent, such as the coroutine monad and the peculiar OpenUnion1. These apparent differences are superficial: mere optimizations. The deep difference emerges only when we try to use both approaches in earnest: adding new effects to already defined ones. That is exactly what we will do in this article.

For the sake of closer comparison, we re-implement the extensible effects within ALCarte. We lose the efficiency of the codensity monad of Extensible Effects and the constant-time injection and projection operations of OpenUnion1. We accept the inconveniences of ALCarte. With the superficial differences eliminated, with the extensible effects being `just' an ALCarte library, a gap emerges. The farther we look into it, the deeper it becomes, separating the two approaches by the modularity and compositionality, or the lack of it. The gap goes to the differences in design. The elegant ideas of catamorphisms and algebras, central to ALCarte, seems to have been counter-productive.

Our plan is thus as follows. First, we recall ALCarte's approach on the example from the paper itself (Section 6), of a stateful computation. We then add a new effect, exceptions -- which trigger a code re-write. Furthermore, two different ways of the state-exception interaction each require its own implementation of the complete effect stack. We stress that we use ALCarte exactly as it was introduced in the JFP 2008 paper. Finally, we replace ALCarte's evaluation algebras with effect handlers. They simplify the code, get rid of the annoying type classes, and bring in modularity. Changing the interaction between the exceptions and the state no longer requires any new code -- rather, a mere change in the order in which the exception and the state handlers are composed.

Version
The current version is July 2014.
References
Wouter Swierstra: Data types à la carte
J. Functional Programming, July 2008, pp. 423-436

Extensible Effects: an alternative to Monad Transformers

Extensible effects and data types a la carte
< http://d.hatena.ne.jp/bigsleep/20140427/1398609185 >
An early implementation of extensible effects within ALCarte. It was the inspiration for the present article.

 

Effectful computations in Data types à la Carte

Let's recall the main ideas of ALCarte. This section re-tells Section 6 of ALCarte, introducing the machinery and the running example for the rest of the present article. Effectful computations are represented by free monads, of the form
     data Term f a = Pure a 
                   | Impure (f (Term f a))
where f is a functor. Furthermore, the functors are built as coproducts
     data (f :+: g) e = Inl (f e) | Inr (g e)
of functors describing individual effects. Section 6 of ALCarte uses a stateful computation to illustrate, where the state is a single memory cell holding an integer. The operation Recall retrieves the contents of the cell and Incr increments it by a given amount:
     data Incr t   = Incr Int t        deriving Functor
     data Recall t = Recall (Int -> t) deriving Functor
Both Incr :: * -> * and Recall :: * -> * are functors acting on the `rest of the computation', represented by the type parameter t. In Recall, the rest of the computation receives an integer, the contents of the memory cell.

To make the effectful operations easier to use, the paper defines smart constructors incr and recall to automatically inject effects into the coproduct (union) type.

     class (Functor sub, Functor sup) => sub :<: sup where
       inj :: sub a -> sup a     -- subtyping witness
     
     inject :: (g :<: f) => g (Term f a) -> Term f a
     inject = Impure . inj
     
     incr :: (Incr :<: f) => Int -> Term f ()
     incr i = inject (Incr i (Pure ()))
     
     recall :: (Recall :<: f) => Term f Int
     recall = inject (Recall Pure)

The following sample term increments the memory cell and returns its old value.

     tick :: Term (Recall :+: Incr) Int
     tick = do  y <- recall
                incr 1
                return y
The paper gives the explicit signature to the term, noting the general signature (which will be inferred if omitted)
     tick' :: (Incr :<: f, Recall :<: f) => Term f Int
     tick' = ... -- the same code as tick
telling that tick' will work in any monad that supports Incr and Recall operations. In contrast, tick works only in the Term (Recall :+: Incr) monad.

All throughout the paper, ALCarte relies on the deep insight relating evaluation with catamorphism, or fold.

     foldTerm :: Functor f => (a -> b) -> (f b -> b) -> Term f a -> b
     foldTerm pure imp (Pure x)     = pure x
     foldTerm pure imp (Impure t)   = imp (fmap (foldTerm pure imp) t)
The second argument of foldTerm, of the type f b -> b, is an algebra, which the paper defines in the form of a type class.
     newtype Mem = Mem Int
     class Functor f => Run f where
       runAlgebra :: f (Mem -> (a,Mem)) -> (Mem -> (a,Mem))
The signature for runAlgebra is chosen to produce the run function of the following type
     run :: Run f => Term f a -> Mem -> (a,Mem)
     run = foldTerm (,) runAlgebra 
The instances of Run tell how to interpret the effectful operations
     instance Run Incr where
       runAlgebra (Incr k r) (Mem i) = r (Mem (i + k))
     
     instance Run Recall where
       runAlgebra (Recall r) (Mem i) = r i (Mem i)
     
     instance (Run f, Run g) => Run (f :+: g) where
       runAlgebra (Inl r) = runAlgebra r
       runAlgebra (Inr r) = runAlgebra r

We can now run tick example

     runtick = run tick (Mem 4)
     -- (4,Mem 5)

Having recalled the ALCarte approach to effects and its running example, we now investigate the extensibility of ALCarte by adding a new effect.

Version
The current version is July 2014.
References
ALaCarte.hs [7K]
The code from the ALCarte paper

 

Problems of adding new effects

This section adds a new effect, exceptions, to the ALCarte's stateful computation example we have just recalled. This hands-on exercise uncovers the serious problem: the lack of modularity. The insight of folds as evaluation, however profound, turns out to be in this case misleading.

It starts simple. The new effect, exceptions of the type e, needs the corresponding functor along with the smart constructor, raise:

     newtype Exc e t   = Exc e   deriving Functor
     
     raise :: (Exc e :<: f) => e -> Term f a
     raise e = inject (Exc e)
That is all that's needed to write programs that use exceptions alongside the already defined effect, state:
     ticke :: (Exc [Char] :<: f, Incr :<: f, Recall :<: f) =>
              Int -> Term f Int
     ticke n = do  y <- recall
                   incr 5
                   z <- recall
                   if z > n then raise "too big" else return y
The shown signature has been inferred by GHC. Mission already accomplished?

The problem creeps up when trying to run ticke. We cannot use the run from the previous section

     run :: Run f => Term f a -> Mem -> (a,Mem)

since it does not know what to do with exceptions, as its type betrays. The result of an effectful computation with exceptions cannot be mere (a,Mem): if an exception is raised the program will fail to produce any value of the type a. Furthermore, there are two ways for exceptions to manifest in the type of the program result. First is Either e (a,Mem), which corresponds to an exception discarding the state; the second result type (Either e a, Mem) is for persistent state; it lets us see the state even if the program finished abnormally. The old evaluation algebra, like the old run,

     class Functor f => Run f where
       runAlgebra :: f (Mem -> (a,Mem)) -> (Mem -> (a,Mem))

does not account for exceptions. Recall, run is meant to be a foldTerm using the evaluation algebra represented by the type class Run. Once the type of run changes a new algebra to fold is needed. We have to define it. Let's start with state-discarding exceptions. The first attempt

     class Functor f => RunEx1 f where
       runEx1Algebra :: f (Mem -> Either e (a,Mem)) -> (Mem -> Either e (a,Mem))

flounders: runEx1Algebra cannot be fully polymorphic in the exception type e. The exception type depends on what the Term f a can actually raise. The algebra hence has to be parameterized with the exception type, to express the relation between f and e.

     class Functor f => RunEx1 e f where
       runEx1Algebra :: f (Mem -> Either e (a,Mem)) -> (Mem -> Either e (a,Mem))

Following the ALCarte paper, we write the instance for the Exc e functor.

     instance RunEx1 e (Exc e) where
       runEx1Algebra (Exc e) _ = Left e
Unfortunately, we also have to write the instances for the other functors! A gap comes to light, between the extensible evaluator (the motivation for ALCarte) and effects. Adding an operation like multiplication to the calculator example in Sections 1-5 of the paper preserves the type of the evaluator: it still computes an integer. Therefore, adding the functor Mul to the existing evaluation algebra suffices. Adding a new effect may change the type of the evaluator, requiring a new algebra, which has to accommodate the new functor and all the old ones. Thus the approach put forth in the ALCarte paper gives us no choice but to write the following boilerplate instances:
     instance RunEx1 e Incr where
       runEx1Algebra (Incr k r) (Mem i) = r (Mem (i + k))
     
     instance RunEx1 e Recall where
       runEx1Algebra (Recall r) (Mem i) = r i (Mem i)
     
     instance (RunEx1 e f, RunEx1 e g) => RunEx1 e (f :+: g) where
       runEx1Algebra (Inl r) = runEx1Algebra r
       runEx1Algebra (Inr r) = runEx1Algebra r
Finally we could run the exceptional computations
     runEx1 :: RunEx1 e f => Term f a -> Mem -> (Either e (a,Mem))
     runEx1 = foldTerm (\a mem -> Right (a,mem)) runEx1Algebra

Trying to run our example runEx1 (ticke 1) reveals another problem -- a type inference failure. The type checker has no way of knowing in which order the functors Incr, Recall and Exc e should appear in the coproduct. The explicit signature and the full type annotation are required:

     runEx1_ticke1 :: Either String (Int, Mem)
     runEx1_ticke1 =
       runEx1 ((ticke 1) :: Term (Exc String :+: (Incr :+: Recall)) Int) (Mem 0)

The programmers will loathe having to write such long type annotations in real programs.

Finally, we have accomplished our goal of adding exceptions to the state computation. Or have we? For exceptions that preserve the program state, the run function should have the type

     runEx2 :: RunEx2 e f => Term f a -> Mem -> (Either e a,Mem)
which is different from the type of runEx1. A new algebra is needed, with its own the complete set of instances for all functors. With two exceptions, one discarding the state and the other preserving, the signature of run and the type of the algebra change once again. We have to rewrite the Run class one more time. Clearly, the approach to effects described in the ALCarte paper is not modular, not composable and does not scale.
Version
The current version is July 2014.
References
ALaCarteExc.hs [3K]
The code for adding exceptions to the ALCarte's sample stateful computation

 

Why effects broke it

ALCarte, motivated by extensible interpreters, described how to assemble the terms to be interpreted and the interpreter itself from separate components. We have seen that when it comes to effects. ALCarte's interpreters are no longer extensible.

The reason for the failure is the central to ALCarte profound idea of evaluation as a fold over the term to interpret:

     run :: Run f => Term f a -> Mem -> (a,Mem)
     run = foldTerm (,) runAlgebra 
This insight leads to the monolithic interpreter, run, which can however be extended through the f-algebra f b -> b described by the type class Run. In theory, adding a new effect, that is, a new factor to the coproduct f, is accommodated just by adding a new instance to Run. This idea works well for simple interpreters like calculators -- but not for effects.

In the stateful computation example of ALCarte, the functor f is (Recall :+: Incr) and and the carrier b of the algebra f b -> b is (Mem -> (a,Mem)). When exceptions are added, (Exc e :+: f) b -> b is no longer an algebra. We have to change the carrier as well, to (Mem -> Either e (a,Mem)). ALCarte has not anticipated such a change.

 

Extensible Effects à la Carte

Modular handling of effects is possible and is actually easy, once we turn away from folds and algebras, however attractive, and use a different set of ideas inspired by Cartwright and Felleisen's modular and compositional approach to effects. This section re-implements Extensible Effects within ALCarte. We use the free monad Term f and the open union, the data type (:+:) and the type class (:<:), as they are. We discard foldTerm and run algebras, replacing them with modular runners, each responsible for handling one particular effect. The resulting implementation is not particularly fast due to the overhead of the free monad -- but it works and it is modular. We demonstrate the extensibility by adding exceptions to a stateful computation. We are able to run the previously defined tick' and ticke exactly as they are -- but without defining and re-redefining any algebras. Different interactions of effects and state are expressed just by functionally composing effects handlers in a different order, without writing any code.

Recall the main ideas from Cartwright and Felleisen's ``Extensible Denotational Language Specifications'':

The free monad

     data Term f a = Pure a 
                   | Impure (f (Term f a))
can be regarded as the message to the authority, the interpreter of the Term f a data type. Impure is the message envelope, carrying a request which includes the `return address'. In the spirit of Cartwright and Felleisen's paper, we start with no effects, represented by the impossible message Void:
     data Void t deriving Functor -- no constructors
     
     ef_run :: Term Void a -> a
     ef_run (Pure x) = x
     -- the Impure alternative cannot happen

ALCarte has already defined the functors for the stateful computation. We repeat them below for reference

     data Incr t   = Incr Int t        deriving Functor
     data Recall t = Recall (Int -> t) deriving Functor
The term Incr n k of the type Incr (Term (Incr :+: r) a) is a proper message, asking the memory authority to increment the memory cell by n and then continue interpreting the term k. The Recall message requests the authority to pass the contents of the memory cell to the return address and interpret the result. What we have just said in English we write in code, as a handler
     ef_runState :: Functor r =>
                    Mem -> Term (Incr :+: (Recall :+: r)) a -> Term r (a,Mem)

The handler is a partial interpreter, which deals only with the Incr and Recall requests leaving the rest for other interpreters. The return type, no longer mentioning Incr and Recall, shows these requests have been dealt with. In short, ef_runState encapsulates the state effect. The implementation is straightforward:

     ef_runState s (Pure x) = return (x,s)
     ef_runState (Mem s) (Impure (Inl (Incr k r))) =
       ef_runState (Mem (s+k)) r
     ef_runState (Mem s) (Impure (Inr (Inl (Recall r)))) =
       ef_runState (Mem s) (r s)
       -- default: leave for others
     ef_runState s (Impure (Inr (Inr t))) = Impure (fmap (ef_runState s) t)
The only notable part is the last clause, dealing with a request that ef_runState does not handle. To understand the clause, let's meditate on the following terms and their types:
     
         Impure (Inr (Inr t)) ::  Term (Incr :+: (Recall :+: r)) a
                 Inr (Inr t)  ::  (Incr :+: (Recall :+: r)) (Term (Incr :+: (Recall :+: r)) a)
                          t   ::  r (Term (Incr :+: (Recall :+: r)) a)
     fmap (ef_runState s) t   ::  r (Term r a)
We see that t is a request for an effect other than Incr and Recall. (Although nothing in ALCarte guards against duplicates in the coproduct functor, the type class (:<:) can be easily modified to add the uniqueness check.) We leave the term holding such a request for other interpreters to handle. When they do and reply to the request, the result is a Term (Incr :+: (Recall :+: r)) a that may still make state requests. However, fmap (ef_runState s) t is a request whose resumption has nothing to do with the state because all such requests will be handled. This extraction of t is the orthogonal projection from the open union, a key feature of Extensible Effects.

The two effect handlers already let us run the tick' example from in the ALCarte introduction -- exactly as it was.

     ef_runtick = ef_run $ ef_runState (Mem 4) tick' 
     -- (4,Mem 5)

Adding exceptions is just as easy, using the previously defined functor Exc e for exceptions of the type e. We merely write the handler for it.

     ef_runExc :: Functor r => Term (Exc e :+: r) a -> Term r (Either e a)
     ef_runExc (Pure x)               = return (Right x)
     ef_runExc (Impure (Inl (Exc e))) = return (Left e)
     -- The default case
     ef_runExc (Impure (Inr t))       = Impure $ fmap ef_runExc t
Again, the last clause is the catch-all for all other effects, leaving them for other handlers. To avoid writing any signatures, we specialize ef_runExc for string exceptions
     ef_runExcS :: Functor r => Term (Exc String :+: r) a -> Term r (Either String a)
     ef_runExcS = ef_runExc
We are ready to run the sample term ticke with exceptions and effects. Here it is again, for reference:
     ticke :: (Exc [Char] :<: f, Incr :<: f, Recall :<: f) =>
              Int -> Term f Int
     ticke n = do  y <- recall
                   incr 5
                   z <- recall
                   if z > n then raise "too big" else return y
It is interesting to watch the result type as we handle the effects one by one:
     :type (ticke 1)
         (Exc [Char] :<: f, Incr :<: f, Recall :<: f) => Term f Int
         -- This program may update the state and raise an exception.
           
     :type ef_runState (Mem 0) (ticke 1)
         Exc [Char] :<: r => Term r (Int, Mem)
         -- The state effects are handled. This program may only raise exceptions.
     
     :type ef_runExcS $ ef_runState (Mem 0) (ticke 1)
         Functor r => Term r (Either String (Int, Mem))
         -- All effects are handled (r is polymorphic). This program can be run.
     
     :type ef_run $ ef_runExcS $ ef_runState (Mem 0) (ticke 1)
         Either String (Int, Mem)
         -- This is the pure computation. It can be evaluated.
     
     ef_run $ ef_runExcS $ ef_runState (Mem 0) (ticke 1)
         Left "too big"

If we wish to preserve the state upon exception, we merely change the order of the handlers in the handler composition. The result type changes accordingly.

     ef_runtickSE1 = ef_run $ ef_runState (Mem 0) $ ef_runExcS (ticke 1)
     -- ef_runtickSE1 :: (Either String Int, Mem)
     -- (Left "too big",Mem 5)
Version
The current version is July 2014.
References
Effectful computations in Data types à la Carte The basics of ALCarte, used as the basis for extensible effects

ALaCarteEff.hs [3K]
The implementation of extensible effects within the ALCarte's framework, with the examples of adding exceptions to the stateful computation

 

Conclusions

We have demonstrated deep similarities and differences between Extensible Effects and Data types à la Carte (ALCarte). Both approaches structure the overall effectful computation as an extensible, open union of individual effects represented by functors. In Extensible Effects, effect interpretation is also modular, expressed as a functional composition of the handlers for individual effects. A particular order of the handlers in the composition encodes a particular interaction of their effects.

In contrast, the ALCarte approach when applied to effects is no longer extensible. The insight from Category Theory (CT) relating evaluation with fold has lead to the monolithic interpreter that proved to be not flexible enough. An idea from Category Theory does not automatically lead to a good design.

Design is a convoluted process; a good solution, however trivial in retrospect, may be difficult to find. Like any other idea, an insight from CT may be productive or counter-productive. Finding a fruitful idea and applying it are hard. It helps to be flexible, avoiding a narrow focus on one small part of CT or one small part of mathematics.



Last updated July 9, 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