Haskellers love monads, and there’s a good reason why. Without monads, Haskell wouldn’t have much of an I/O system at all, as Simon Peyton-Jones described it, it was embarassing to note that the emperor lacked I/O at conferences. Nevertheless, Haskell could be considered the world’s finest imperative language because of the way its type system forces one to separate purity and impurity, allowing the use of pure functions in impure code, but not vice versa.

The next stepping stone on the road to Haskell proficiency is often learning monad transformers, so that effects can be combined. In other words, we want to write code like this, resembling an impure language.

``````ticke n = do y <- recall
incr 5
z <- recall
if z > n
then raise "too big"
else return y
``````

But this blog post is not about monad transformers, it’s about another idea that’s less well-known, free monads, a neat way to combine effects with less boilerplate, and has been applied in works such as Extensible Effects and Polysemy.

This blog post assumes a working knowledge of Haskell, typeclasses, and some category theory.

## What is a free object?

A free object is a construction that obeys the axioms for that object, generated from something simpler. A canonical example of a free object is a free monoid. Recall the axioms for monoids (expressed as a typeclass in Coq):

``````Class Monoid { A : Type } (op : A -> A -> A)(unit : A) : Type :=
{ op_assoc : forall x y z : A, op x (op y z) = op (op x y) z;
unit_left : forall x, op unit x = x;
unit_right : forall x, op x unit = x }.
``````

`op_assoc` states that the operation must be associative, and `unit_left` and `unit_right` state that the element `unit` acts as an identity on the left and right for any `x` in the set respectively.

So, given a set `S = {a, b, c, d}`, what is the free monoid over it? It’s simply the language `{a, b, c, d}*`, giving us strings like `""`, `"aa"`, `"abc"`, `"acdbcd"` and so on. The only thing we can do with these objects is treat them according to the axioms they obey, in other words, we can only concatenate them and nothing more.

People who have written interpreters may notice that free objects are like valid ASTs of a particular programming language. The axioms let us perform some manipulations, for instance, if we create a free group, we know we can rewrite `a * a^-1` to `unit`, because that’s one of the group axioms. However, we would be unable to reduce something like `2+3` because we don’t have an interpretation for it. This will come in later when we implement interpreters for effects.

Enough of this abstract algebra, let’s see some code!

## Coproducts of functors

``````infixr :+:
data (f :+: g) r = Inl (f r)
| Inr (g r)
deriving (Functor)
``````

`:+:` is a type operator, i.e. it takes two type constructors ```f :: * -> *``` and `g :: * -> *` and a type `r :: *`, and producing a new type `(f :+: g) r :: *`. To construct a value of this type, we the `Inl` and `Inr` constructors. This resembles the `Either` type, but over higher kinded types `f` and `g`. Categorically, this is the coproduct construction in the functor category.

Now the main data type:

``````data Term f a = Pure a
| Impure (f (Term f a))
``````

We can read `Term f a` as a term of our language generated by `f`, having a final value of type `a`, here are some examples.

``````λ> Pure 3
Pure 3 :: Term f Integer
λ> Impure (Just (Pure 3))
Impure (Just (Pure 3)) :: Term Maybe Integer
λ> Impure Nothing
Impure Nothing :: Term Maybe a
``````

But generated how? Notice that the argument to `Impure` has type ```f (Term f a)```, but we’re showing how to construct a term of type `Term f a` in the `data` declaration, so this is like fixpoints of functions, with `Pure` as the “base case”. In the case that `f` happens to be a functor, `Term` is what is known as a fixpoint of a functor, as seen in papers such as Data types à la carte by Swierstra.

It gets better. If we know `f` is a functor, we know that it must have `fmap`, even better, we can write the `Functor`, `Applicative` and `Monad` instances for `Term f`!

``````instance Functor f => Functor (Term f) where
fmap f (Pure x) = Pure \$ f x
fmap f (Impure t) = Impure \$ fmap (fmap f) t

instance Functor f => Applicative (Term f) where
pure = Pure
Pure f <*> Pure x = Pure \$ f x
Pure f <*> Impure b = Impure \$ fmap (fmap f) b
Impure fx <*> a = Impure \$ fmap (<*> a) fx

instance Functor f => Monad (Term f) where
return = pure
Pure x >>= f = f x
Impure t >>= f = Impure \$ fmap (>>= f) t
``````

At first sight this looks scary, but in fact it isn’t at all, here’s the same code with only the last line in each instance declaration shown.

``````instance Functor f => Functor (Term f) where
-- ...
fmap f (Impure t) = Impure \$ fmap (fmap f) t

instance Functor f => Applicative (Term f) where
-- ...
Impure fx <*> a = Impure \$ fmap (<*> a) fx

instance Functor f => Monad (Term f) where
-- ...
Impure t >>= f = Impure \$ fmap (>>= f) t
``````

Notice how we’re implementing `>>=` with `>>=` on the right, and `<*>` with `<*>`, but applying it via `fmap`? It seems like an impossible trick at first, we don’t even know `f` forms a monad! But we do know some laws about applicatives and monads.

``````fmap f (pure x) = pure (f x)
pure f <*> pure x = pure (f x)
pure x >>= f = f x
``````

Believe it or not, this is exactly the code we need to implement the `fmap`, `<*>` and `>>=` operators for `Term f`! Perhaps the only thing left to explain is the implementation of `<*>` in the case that the first argument is pure and the second argument is impure, left as an exercise.

``````Pure f <*> Impure b = Impure \$ fmap (fmap f) b
``````

We’re quite close now, just one more class and a couple of instances and we’ll have the core for our free monad effects library.

``````class (Functor sub, Functor sup) => sub :<: sup where
inj :: sub a -> sup a
``````

`sub` and `sup` are functors, and `inj` is the natural transformation that turns a `sub` into a `sup`. Intuitively we can think of `sup` as allowing an embedding of `sub` into it, but not necessarily the other way around. Now that we’re in the functor category, we know there is an identity natural transformation for every functor into itself, so there must be an embedding of every functor into itself.

``````instance Functor f => f :<: f where
inj = id
``````

What about the relation between `f` and `f :+: g`? Now that we’re talking category theory, `f :+: g` is really a coproduct of `f` and `g` in the functor category. So indeed there is a morphism from `f` to `f :+: g`, the `Inl` morphism.

``````instance (Functor f, Functor g) => f :<: (f :+: g) where
inj = Inl
``````

Finally, we want to be able to extend an existing embedding. Let’s say we are given functors `f`, `g` and `h`, and know that `f :<: g`. It stands to reason that if `f` already has an embedding into `g`, it also has an embedding into whatever `g` can embed into. In particular, `g` can embed into `h :+: g`. Therefore, `f` can be embedded into `h :+: g` as well. First we embed `f` into `g` via `inj`, then we go from `g` to `h :+: g` by `Inr`. `inj` and `Inr` are natural transformations, so we can compose them to get a natural transformation from `f` to `h :+: g`.

``````instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (h :+: g) where
inj = Inr . inj
``````

First, we’re going to want to convert a `Term f a` into an `a`, i.e. escaping out of the `Term` monad. We can extract such an `a` by pattern matching on `Pure a`. It now remains to settle on an appropriate functor `f`. We don’t want to handle the `Impure` case, because that means we have some function of type `f a -> a`, which may not exist (e.g. `[]`, `IO`, `Maybe`). Since `Impure` should not happen, `f (Term f a)` must not happen either, which means `a -> f a` should not exist!

A functor `f` with no way of getting from `a -> f a` nor `f a -> a`? This forces our choice of `f` to be the `Void` functor, which has no constructors.

``````data Void t
deriving (Functor)

efRun :: Term Void a -> a
efRun (Pure a) = a
``````

And that’s it. While it looks like boilerplate, we can more or less mechanically write out the instances, thanks to universal objects, and notions from category theory. To really illustrate the power of this, we’re going to see a series of increasingly ambitious examples of effects.

## A stateful calculator

Let’s implement a simple calculator with a single `Int` register. We define the operations of this calculator separately; `Incr` and `Reader`.

• `Incr i t` increments the state by `i` and returns `t`
• `Reader f` extracts the state and runs `f` on it
• `Mem i` represents the state having value `i`
``````data Incr t = Incr Int t deriving (Functor)
data Mem = Mem Int deriving (Show)
``````

Given the commands, we need to define their denotation, i.e. their meaning. This is given by the `efRunCalc` function.

If the command is `Pure x`, just return `x` along with the state.

``````efRunCalc :: Functor r => Mem
-> Term (Incr :+: (Reader :+: r)) a
-> Term r (a, Mem)
efRunCalc s (Pure x) = return (x, s)
``````

If the command is `Incr k r`, modify the state by `k` and continue with r. The slight twist is that we need to pattern match with `Inl`, because to extract `Incr` from `(Incr :+: (Reader :+: r))`. To extract `Reader` from `(Incr :+: (Reader :+: r))` we have to perform `Inl` followed by `Inr`. Finally, to handle `r`, we ```fmap (efRunCalc s)``` over `t`.

``````efRunCalc (Mem s) (Impure (Inl (Incr k r))) = efRunCalc (Mem (s + k)) r
efRunCalc (Mem s) (Impure (Inr (Inl (Reader r)))) = efRunCalc (Mem s) (r s)
efRunCalc s (Impure (Inr (Inr t))) = Impure (efRunCalc s <\$> t)
``````

We’ll also define a couple of helper functions, `incr` and `recall` can be thought of the user-facing functions for calculator effects.

``````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 :: (Reader :<: f) => Term f Int
``````

Now, we can combine our `Incr` and `Reader` effects in a single monad.

``````tick :: (Incr :<: f, Reader :<: f) => Term f Int
tick = do
y <- recall
incr 1
return y
``````

What you see in the code examples is all there is, no monad transformers needed. We can combine effects freely. When we interpret effects, we handle them one by one.

``````λ> tick & efRunCalc (Mem 4) & efRun
(4,Mem 5)
``````

Suppose now we want to add a `raise` command to our calculator, the `Exc` effect. This is done separately. A pattern raises for making new effects, we define our type, our user-facing functions and an interpreter for our effect.

``````data Exc e t = Exc e deriving Functor

raise :: (Exc e :<: f) => e -> Term f a
raise e = inject (Exc e)

efRunExc :: Functor r => Term (Exc e :+: r) a -> Term r (Either e a)
efRunExc (Pure x) = return (Right x)
efRunExc (Impure (Inl (Exc e))) = return (Left e)
efRunExc (Impure (Inr t)) = Impure (efRunExc <\$> t)
``````

Due to our coproduct construction, `Exc` is separate from the other effects. `ticke` uses all the effects we have seen so far.

``````ticke :: (Exc String :<: f, Incr :<: f, Reader :<: f) => Int -> Term f Int
ticke n = do y <- recall
incr 5
z <- recall
if z > n
then raise "too big"
else return y

efRunExcString :: Functor r => Term (Exc String :+: r) a
-> Term r (Either String a)
efRunExcString = efRunExc
``````

The reason why we need `efRunExcString` is that we need to be explicit about handling the `Exc String` effect, otherwise we get a type error about no instances for `(Exc String :<: Void)`. It’s really a type inference failure, because Haskell could not infer the instance at the call-site (this is a problem effect libraries attempt to address).

``````λ> ticke 1 & efRunExcString & efRunCalc (Mem 0) & efRun
(Left "too big",Mem 5)
``````

For our final example, we generalize the state to an arbitrary type `s`, and write an imperative program to sum the first `n` numbers.

``````-- Enable the ConstraintKind language extension for this
type StEff s r = (Reader s :<: r, Writer s :<: r)

efRunSt :: Functor r => State s -> Term (St s r) a -> Term r (a, s)
efRunSt (State s) (Pure x) = return (x, s)
efRunSt (State s) (Impure (Inl (Put k r))) = efRunSt (State k) r
efRunSt (State s) (Impure (Inr (Inl (Get r)))) = efRunSt (State s) (r s)
efRunSt s (Impure (Inr (Inr t))) = Impure (efRunSt s <\$> t)

put :: (Writer s :<: f) => s -> Term f ()
put s = inject (Put s (Pure ()))

get :: (Reader s :<: f) => Term f s
get = inject (Get Pure)

sumN :: (StEff (Integer, Integer) f) => Term f ()
sumN = do (acc, n) <- get
if n == 0
then return ()
else do { put (acc + n, n - 1); sumN }

sumNEx :: ((), (Integer, Integer))
sumNEx = sumN
& efRunSt (State (0,10))
& efRun
``````