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.
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
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.
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.
data Term f a = Pure a | Impure (f (Term f a))where
fis 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
Recallretrieves the contents of the cell and
Incrincrements it by a given amount:
data Incr t = Incr Int t deriving Functor data Recall t = Recall (Int -> t) deriving FunctorBoth
Incr :: * -> *and
Recall :: * -> *are functors acting on the `rest of the computation', represented by the type parameter
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
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 yThe 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 ticktelling that
tick'will work in any monad that supports
Recalloperations. In contrast,
tickworks 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
runAlgebrais chosen to produce the
runfunction of the following type
run :: Run f => Term f a -> Mem -> (a,Mem) run = foldTerm (,) runAlgebraThe instances of
Runtell 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
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.
It starts simple. The new effect, exceptions of the type
the corresponding functor along with the smart constructor,
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 yThe shown signature has been inferred by GHC. Mission already accomplished?
The problem creeps up when trying to run
ticke. We cannot
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
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
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))
runEx1Algebra cannot be fully polymorphic in the exception
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
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 eUnfortunately, 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
Multo 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 rFinally 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
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
runand the type of the algebra change once again. We have to rewrite the
Runclass one more time. Clearly, the approach to effects described in the ALCarte paper is not modular, not composable and does not scale.
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 (,) runAlgebraThis insight leads to the monolithic interpreter,
run, which can however be extended through the f-algebra
f b -> bdescribed 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
(Recall :+: Incr) and and the carrier
b of the algebra
f b -> b
(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.
Term fand the open union, the data type
(:+:)and the type class
(:<:), as they are. We discard
foldTermand 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
tickeexactly 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 adata type.
Impureis 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
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 FunctorThe term
Incr n kof the type
Incr (Term (Incr :+: r) a)is a proper message, asking the memory authority to increment the memory cell by
nand then continue interpreting the term
Recallmessage 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
Recall requests leaving the rest for other interpreters.
The return type, no longer mentioning
these requests have been dealt with.
ef_runState encapsulates the state effect. The implementation
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_runStatedoes 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
tis a request for an effect other than
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)) athat may still make state requests. However,
fmap (ef_runState s) tis a request whose resumption has nothing to do with the state because all such requests will be handled. This extraction of
tis 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
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 tAgain, the last clause is the catch-all for all other effects, leaving them for other handlers. To avoid writing any signatures, we specialize
ef_runExcfor string exceptions
ef_runExcS :: Functor r => Term (Exc String :+: r) a -> Term r (Either String a) ef_runExcS = ef_runExcWe are ready to run the sample term
tickewith 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 yIt 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)
The implementation of extensible effects within the ALCarte's framework, with the examples of adding exceptions to the stateful computation
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.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML