# Free Monads from Scratch

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.

## Free Monads

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
`Recall`

.

`Incr i t`

increments the state by`i`

and returns`t`

`Recall 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 Recall t = Recall (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 :+: (Recall :+: 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 :+: (Recall :+: r))`

. To
extract `Recall`

from `(Incr :+: (Recall :+: 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 (Recall 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 :: (Recall :<: f) => Term f Int
recall = inject (Recall Pure)
```

Now, we can combine our `Incr`

and `Recall`

effects in a single monad.

```
tick :: (Incr :<: f, Recall :<: 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)
```

## Adding Exceptions

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, 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
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
```

## Conclusion and Further Reading

I hope this post was illuminating in understanding what free monads are and their implementation. There’s quite a lot of literature on the subject, and the various effect libraries in use are worth checking out, because they address problems we weren’t able to handle in our from-scratch implementation, reducing boilerplate even further, creating better error messages, among other things.

- Data types à la carte
- The paper by Swierstra in which he presents a solution to the
*expression problem*, that is, extending a data type without recompiling existing code while retaining type safety.*Data types à la carte*expresses effects as algebras and interpretation as a fold over that algebra.

- The paper by Swierstra in which he presents a solution to the
- Extensible Effects vs Data types à la Carte
- While Swierstra’s construction is notable, Oleg Kiselyov
demonstrates that the algebra construction is unable to handle the
addition of new effects, in other words, it was not an
*extensible*system. Provides some good precautions on using category theory as a design tool.

- While Swierstra’s construction is notable, Oleg Kiselyov
demonstrates that the algebra construction is unable to handle the
addition of new effects, in other words, it was not an