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
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.
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 f is a functor. Furthermore, the functors are built as coproductsdata (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.
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.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.
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)
ALaCarteEff.hs [3K]
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-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML