Freer Monads, More Extensible Effects
1. Derivation of Free-er Monad
1.1 Reader Effect
Reader
computations depend on a value supplied by the environment/context. A side-effect can be understood as an interaction of an expression with its context. The possible requests of a Reader
can be specified as a data type.
data It i a = Pure a
| Get (i -> It i a)
The expression Pure e
marks the computation e
that makes no requests, silently working towards a value of the type a
. The request Get k
asks the context for the (current dynamically-bound) value of type i
. Having received the value i
, the computation k i :: It i a
continues (just the same as monadic binding works), perhaps asking for more values from the context. The argument k
in Get k
can hence be called a continuation.
The simplest asking computation is ask
, which immediately returns the received value from the context`:
ask :: It i i
ask = Get Pure
Larger computations are built with the help of >>=
.
instance Monad (It i) where
return :: a -> It i a
return = Pure
(>>=) :: It i a -> (a -> It i b) -> It i b
Pure x >>= = k x
Get k' >>= k = Get (k' >>> k)
The last clause in the definition of bind says that: “a computation that waits for an input and then continues as k
”, and after that, continues as k
" is the same as “a computation that continues after waiting as the composition of k'
and k
”. The Kleisli composition operation (>>>)
is the composition of effectful functions.
(>>>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
Here are two examples of bigger Reader computations.
addGet :: Int -> It Int Int
addGet = ask >>= \i -> return (i + x)
addN :: Int → It Int Int
addN n = foldl (>>>) return (replicate n addGet) 0
The computations addGet
and addN
make requests to the context. We need to define how to reply to a request, that is, how to “run” these computations.
The following interpreter runReader
gives the same value i
on each request; the type It i
is hence interpreted as the Reader
monad.
runReader :: i -> It i a -> a
runReader _ (Pure v) = v
runReader x (Get k) = runReader x (k x)
Unlike how the MTL Reader works, It i a
can choose to be interpreted in a different way. For example, if we wanted each request to get a new value as if read from an input stream:
feedAll :: [i] -> It i a -> a
feedAll _ (Pure v) = v
feedAll [] _ = error "end of stream"
feedAll (x : xs) (Get k) = feedAll xs (k x)
2.2 Reader/Writer Effect
We now add another effect - rather than asking a context for a value, we tell the context. This is a Writer.
data IT i o a = Pure a
| Get (i -> IT i o a)
| Put o (() -> IT i o a)
The Put o k
requests tells the value o
to the context. The context then acknowledges this with ()
, and afterwards, the computation continues as k ()
(i.e. a continuation k
which is passed ()
as an argument).
IT i o
is also a monad:
instance Monad (IT i o) where
return = Pure
Pure x >>= k = k x
Get k' >>= k = Get (k' >>> k)
Put x k' >>= k = Put x (k' >>> k)
Again, the last clause in the definition of bind says that: “a computation that tells the context and continues as k
, and then as k
” is the same as “a computation that tells the context and continues as the composition of k'
and k
”.
In the MTL
version of the Writer
monad, the told value must have a Monoid
type. In contrast, IT i o
has no such constraints. If we wanted to write an interpreter for IT
which interpreted it as a Writer
which accumulates the told values in a monoid, we could do so by adding the monoid constraint to the interpreter.
runRdWriter :: Monoid o => i -> IT i o a -> (a, o)
runRdWriter i m = loop mempty m
where
loop acc (Pure x) = (x, acc)
loop acc (Get k) = loop acc (k i )
loop acc (Put o k) = loop (acc `mappend` o) (k ())
The IT i o
computation is an extension of It i
. Data types are themselves not extensible, therefore, we have to change the data type name and modify the signatures of addGet
and addN
, even if their code does not care about the new writer effect and remains essentially the same.
2.3 Free Monad
A data type describing an effectful computation such as It i a
and IT i o a
follows a common pattern: It is a recursive data type, with the Pure
variant for the absence of any requests, and variants for requests (which usually contain the continuation that receives the reply, except for exceptions that do not expect any reply).
This pattern of pure and effectful parts and covariant recursive occurrences can be captured as the Free monad, where f
is a functor (that is, in f a
, the type a
occurs covariantly).
data Free f a = Pure a
| Impure (f (Free f a))
Rather than having to keep writing new instances for each new effect and each combination of effects (like for It i
and IT i o
), the Free f
data type lets us capture the common pattern:
instance Functor f => Monad (Free f) where
return = Pure
Pure a >>= k = k a
Impure f >>= k = Impure (fmap (>>= k) f)
instance Functor f => Applicative (Free f) where
pure = Return
Pure f <*> as = fmap f as
Impure faf <*> as = Impure (fmap (<*> as) faf)
For a functor f
, Free f
is the free monad; new effects will have new effect signatures f
, but the single instance of Monad (Free f)
will work for all of them, with no further rewriting.
As an example, the earlier IT i o
computation may now be specified as:
data ReaderWriter i o x = Get (i -> x) | Put o (() -> x)
instance Functor (ReaderWriter i o) where
...
type IT i o a = Free (ReaderWriter i o) a
In general monads do not compose: if M1 a
and M2 a
are monads, M1 (M2 a)
is generally not. Free monads however are a particular form of monads, defined via a functor. Functors do compose.
2.4 Free-er Monads
Let’s look more carefully at the Monad instance for Free f
.
instance Functor f => Monad (Free f) where
return = Pure
Pure a >>= k = k a
Impure f >>= k = Impure (fmap (>>= k) f)
The purpose of fmap
here is to extend the continuation, embedded somewhere within f (Free f a)
, by (>>>)
-composing it with the new k
. This hence composes all of the effectful continuations found nested within the free monad. The operation fmap
lets us generically modify the embedded continuation, for any request signature.
Since the continuation argument is being handled so uniformly, it makes sense to take it out of the request signature (e.g. Get (i -> x)
and Put o (() -> x)
) and place it into the fixed request data structure (i.e. as the second argument of the Impure
constructor of FFree f a
):
data FFree f a where
Pure :: a -> FFree f a
Impure :: f x -> (x -> FFree f a) -> FFree f a
The first argument of the request signature, f x
, tells us the type x
of the reply, to be fed into the continuation. Different requests have their own reply types, hence x
is existentially quantified.
The monad instance for FFree f
no longer needs the Functor
constraint on f
.
- Previously with
Free f
and its associated constructorImpure (f (Free f a))
, in order to extend the continuation, we had tofmap
the bind of the continuation>>= k
into thef (Free f a))
embedded in theImpure
constructor – this is because the continuation we’re extending is found insidef (Free f a))
. - Now with
FFree f
and its associated constructorImpure :: f x -> (x -> FFree f a) -> FFree f a
, because we already have access to the current continuation (as the second argument ofImpure
), we no longer need tofmap
over anything – we can directly take the continuationk' :: (x -> FFree f a)
and compose it with the new continuationk :: (a -> FFree f b)
.
instance Monad (FFree f) where
Impure fx k' >>= k = Impure fx (k' >>> k)
FFree f
is more satisfying than Free f
, because it abstracts more of the common pattern of accumulating continuation. It is more general, not imposing any constraints on f
– it is “freer”.
Our Reader-Writer effect then gets the following signature:
data FReaderWriter i o x where
Get :: FReaderWriter i o i
Put :: FReaderWriter i o ()
It is a GADT: the type variable x
in FReaderWriter i o x
is instantiated depending on the type of the request.
The type IT i o a
can now be represented using the new FFree
monad.
type IT i o a = FFree (FReaderWriter i o) a
Continuing this example of State s
(i.e. ReaderWriter), we can now forget not only return
and bind
, but also the fmap
operation, and still recover the state monad through the FFree (State s)
construction (where types i
and o
have been unified as s
). This means we no longer have to bother defining the basic monad and fu nctor operations in the first place. We now get not only the Monad
instance for free, but also the Functor
and Applicative
instances.
Advantages:
- Because the continuation can now be accessed directly (rather than via
fmap
which has to rebuild the mapped data structure), the Freer monad is more economical in terms of memory and run-time. - The explicit continuation in
FFree
makes it easier to change its representation.
2.5 Free-er Functors
We can show another derivation of FFree
. Recall that if f :: * -> *
is a functor, we can convert f x
to f a
whenever we can map x
values to a
values. If g :: ∗ -> ∗
is not a functor, such a conversion is not possible. We can “cheat” however: although we cannot truly fmap h :: x -> a
over g x
, we can keep its two operands h
& g x
as a pair, and assume the mapping as if it were performed:
data Lan (g :: ∗ -> ∗) a where
FMap :: (x -> a) -> g x -> Lan g a
Any further mapping over Lan g a
would update the original mapping (x -> a)
, leaving g x
intact. That is, Lan g
is now a formal functor:
instance Functor (Lan g) where
fmap h (FMap h' gx) = FMap (h ◦ h') gx
One may think of this as a free Haskell Functor. We can show that if we substitute Lan g
as f
in Impure (f (Free f a))
of Free f
, we get:
Impure :: (x -> (Free (Lan g) a)) -> g x -> Free (Lan g) a
This is the type of FFree.Impure
! Hence, we have:
type FFRee g = Free (Lan g)
2.6 From Free(er) Monads to Extensible Effects
The form of free monads, built from functors, lends itself to composability since functors compose. This section demonstrates this composability on freer monads.
There are two sides to composability: extensible monad types and modular interpreters.
A monad type is extensible if we can add a new effect without having to touch or even recompile the old code. The Free f
or FFree f
lets us do that by the monad type being indexed by the request signature f
. In contrast, specifying this signature as an ordinary data type, such as ReaderWriter
or the GADT FReaderWriter
is not extensible because an ordinary variant data type is a closed union, having a fixed number of variants.
To represent open unions, we will use the abstract type:
Union (r :: [∗ -> ∗]) x
- The first argument
r
is a type-level list of effect labels. It lists all effects that are possible in a computation. - The second argument
x
is the response type, which depends on a particular request.
A concrete Union r x
value contains one request out of those listed in r
.
In order to achieve extensibility, we must be able to talk about one effect without needing to list all the others, i.e. we need effect polymorphism. To do this, our implementation provides a type class:
class Member t r where
inj :: t v -> Union r v
prj :: Union r v -> Maybe (t v)
This asserts that an effect label t
occurs in the list r
. If an effect is part of the union, its request can be injected and projected.
Another function, decomp
, is provided to orthogonally project from the union, allowing us to decompose the union into either a request labelled t
, or a smaller union without t
.
The extensible freer monad, the monad of extensible effects, is hence FFree
with f x
replaced by the open union Union r x
, containing all possible effects:
data FEFree r a where
Pure :: a -> FEFree r a
Impure :: Union r x -> (x -> FEFree r a) -> FEFree r a
A request label defines a particular effect and its requests. For example, the Reader and Writer effects have the following labels:
data Reader i x where
Get :: Reader i i
data Writer o x where
Put :: o -> Writer o ()
We have split the FReaderWriter
request signature into its components, to be combined in the open union.
The simplest Reader
computation, ask
, can now be written as:
ask :: Member (Reader i) r => Eff r i
ask = Impure (inj Get) return
The signature tells us that ask
is an Eff r i
computation which includes the Reader i
effect, without telling us what other effects may be present. Unlike the previous version of ask
, the new one can be used extensibly in programs with other effects.
2.7 Performance Problem of Free(er) Monads
Free and freer monads are poorly performing. Let’s re-examine the FFree f
monad instance.
data FEFree r a where
Pure :: a -> FEFree r a
Impure :: Union r x -> (x -> FEFree r a) -> FEFree r a
instance Monad (FFree f) where
Impure fx k' >>= k = Impure fx (k' >>> k)
The bind operation traverses its left argument, but merely passes around the right argument. Therefore, the performance of left-associated binds will be algorithmically poor – just like the performance of left-associated list appends is poor.
Consider the definition of (++)
.
(++) :: [a] -> [a] -> [a]
(++) [] ys = ys
(++) (x:xs) ys = x : (++) xs ys
From the definition of (++)
, the performance is linear in the length of the left-hand-side list xs
. Note how we never need to process the right-hand-side list ys
.
Now let’s examine how [1, 2, 3] ++ [4, 5, 6] ++ [7, 8, 9]
is evaluated.
If (++)
were right associative (which it is), then we would have to evaluate [1, 2, 3] ++ ([4, 5, 6] ++ [7, 8, 9])
.
- We first evaluate the second append,
([4, 5, 6] ++ [7, 8, 9])
. This involves processing4
,5
, and6
. - We then evaluate the first append
[1, 2, 3] ++ [4, 5, 6, 7, 8, 9]
. This involves processing1
,2
, and3
.
If (++)
were left associative, then we would evaluate ([1, 2, 3] ++ [4, 5, 6]) ++ [7, 8, 9]
:
- To evaluate the first append,
([1, 2, 3] ++ [4, 5, 6])
, we would need to process1, 2, 3
. - To then evaluate the second append,
[1, 2, 3, 4, 5, 6] ++ [7, 8, 9]
, we would need to process1, 2, 3, 4, 5, 6
– this performance is quadratic because we’re reprocessing the same elements again.
3. Final Result: Freer and Better Extensible Eff Monad
This describes the current, improved and efficient library of extensible effects.
3.1 Composed Continuation as a Data Structure
The new library is based on the FEFree monad
we previously derived.
data FFree f a where
Pure :: a -> FFree f a
Impure :: f x -> (x -> FFree f a) -> FFree f a
However, it differs in one final respect: Now that the request continuation, (x -> FFree f a)
, is exposed, it can be represented in other ways than just a function. The motivation for a new representation comes from looking at the monad instance for FEFree f
, which extends the request continuation k'
with the new segment k
.
instance Monad (FFree f) where
Impure fx k' >>= k = Impure fx (k' >>> k)
The aim is to represent this conceptual sequence of extending the continuation with more and more segments, as a concrete sequence. It would contain all the segments that should be functionally composed – without actually composing them.
We call the improved FEFree r
monad Eff r
, where r
is the list of effect labels. The request continuation, which receives the reply x
and works towards the final answer a
, then has the type x -> Eff r a
. We define the convenient type abbreviation for such effectful functions, that is, functions mapping a
to b
that also do effects denoted by r
.
type Arr r a b = a -> Eff r b
The job of the monad bind is to accumulate the request continuation, by (>>>)
-composing it with further and further Arr r a b
segments. Rather than really doing the (>>>)
-composition, we assume it as performed, and merely accumulate the pieces being composed in a data structure. The data structure has to be heterogenous and type-aligned: the Arr r a b
being composed must have different a
and b
types, and the result type of one function must match the argument type of the next.
We choose the sequence FTCQueue
of the following interface.
The type FTCQueue m a b
represents the composition of one or more functions of the general shape a -> m b
. It is a non-empty tree.
data FTCQueue (m :: ∗ -> ∗) a b where
Leaf :: (a -> m b) -> FTCQueue m a b
Node :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
The operation tsingleton
constructs a one-element sequence.
tsingleton :: (a -> m b) -> FTCQueue m a b
tsingleton = Leaf
The operation (▶)
adds a new element at the right, i.e. it extends the sequence with a new request continuation. It is much like snoc
.
(▶) :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
t ▶ r = Node t (Leaf r)
The operation (▶◀)
concatenates two sequences.
(▶◀) :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
t1 ▶◀ t2 = Node t1 t2
The type ViewL m a b
allows us to perform left-edge deconstruction on an FTCQueue
.
data ViewL m a b where
TOne :: (a -> m b) -> ViewL m a b
(:|) :: (a -> m x) -> (FTCQueue m x b) -> ViewL m a b
The function tviewl
removes the element from the left edge of a sequence.
tviewl :: FTCQueue m a b -> ViewL m a b
tviewl (Leaf r) = TOne r
tviewl (Node t1 t2) = go t1 t2
where
go :: FTCQueue m a x -> FTCQueue m x b -> ViewL m a b
go (Leaf r) tr = r :| tr
go (Node tl1 tl2) tr = go tl1 (Node tl2 tr)
All operations have constant or average constant running time. Our FTCQueue
may be regarded as the minimalistic version of a more general fast type-aligned queue.
The composition of functions (continuation segments), a -> Eff r t1
, t1 -> Eff r t2
, tn -> Eff r b
, is represented as:
type Arrs r a b = FTCQueue (Eff r) a b
It is a sequence of continuation segments between Eff r
monads.
The Eff r
monad has the following form:
data Eff r a where
Pure :: a -> Eff r a
Impure :: Union r x -> Arrs r x a -> Eff r a
The type Arrs r a b = FTCQueue (Eff r) a b
is isomorphic to the single type Arr r a b = a -> Eff r b
, just like a composition of functions is a function itself.
-
In one direction, the
singleK
conversion takes one element and builds a sequence of effectful continuations.-- :: (a -> Eff r b) -> FTCQueue (Eff r) a b singleK :: Arr r a b -> Arrs r a b singleK = tsingleton -- tsingleton :: (a -> m b) -> FTCQueue m a b
-
In the other direction, the
qApp
operation applies the argumentx
to a composition of functions denoted by the sequenceArrs r a b
.-- type Arrs r a z = FTCQueue (Eff r) a z qApp :: Arrs r a z -> a -> Eff r z -- tviewl :: FTCQueue (Eff r) a z -> ViewL (Eff r) a z -- q :: FTCQueue (Eff r) a z qApp q x = case tviewl q of -- k :: a -> Eff r z TOne k -> k x -- k :: a -> Eff r b -- t :: (FTCQueue (Eff r) b z) k :| t -> bind' (k x) t where bind' :: Eff r b -> Arrs r b z -> Eff r z bind' (Pure y) k = qApp k y bind' (Impure u q) k = Impure u (q ▶ k)
More precisely, it applies
x
to the headk
of the sequence of effectful continuationsq
to create an effect – if there exists a tailt
of this sequence, it takes this effect and tacks on the tail to produce a new effect.That is the performance advantage of the new representation for continuation. The
bind'
operation is like the monad bind(>>=)
but with the continuation represented as the sequenceArrs r a b
rather than thea -> Eff r b
function.If the application
k x
runs in constant time, the wholeqApp q x
takes on average constant time.
Finally, in the monad instance of Eff r
, the bind operation grows the sequence of continuations Arrs r x a
by appending another continuation k
with (▶)
(rather than composing with (>>>)
), which takes constant time.
instance Monad (Eff r) where
return = Pure
Pure x >>= k = k x
Impure u q >>= k = Impure u (q ▶ k)