Probabilistic Effects. λθ

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 constructor Impure (f (Free f a)), in order to extend the continuation, we had to fmap the bind of the continuation >>= k into the f (Free f a)) embedded in the Impure constructor – this is because the continuation we’re extending is found inside f (Free f a)).
  • Now with FFree f and its associated constructor Impure :: f x -> (x -> FFree f a) -> FFree f a, because we already have access to the current continuation (as the second argument of Impure), we no longer need to fmap over anything – we can directly take the continuation k' :: (x -> FFree f a) and compose it with the new continuation k :: (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 processing 4, 5, and 6.
  • We then evaluate the first append [1, 2, 3] ++ [4, 5, 6, 7, 8, 9]. This involves processing 1, 2, and 3.

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 process 1, 2, 3.
  • To then evaluate the second append, [1, 2, 3, 4, 5, 6] ++ [7, 8, 9], we would need to process 1, 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 argument x to a composition of functions denoted by the sequence Arrs 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 head k of the sequence of effectful continuations q to create an effect – if there exists a tail t 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 sequence Arrs r a b rather than the a -> Eff r b function.

    If the application k x runs in constant time, the whole qApp 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)
Last updated on 13 Nov 2020
Published on 13 Nov 2020