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 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 Reader t = Reader (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
recall = inject (Reader Pure)

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)

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

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.
  • 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.