# Free monad transformers

This post explains categorically the free construction of *free monad transformers* which can be found in the `free`

library on Hackage.

```
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Free.Monad.Trans where
import Control.Monad
```

Monad transformers are represented by the following type class. `lift`

is a monad morphism between `m`

and `t m`

. `monadTrans`

witnesses the fact that a monad transformer transforms monads into monads; it is not as general as it could be, but we will not need any more power here.

```
class MonadTrans t where
lift :: Monad m => m a -> t m a
monadTrans :: Monad m => (Monad (t m) => t m a) -> t m a
```

`FreeT`

is a functor

```
newtype FreeT f m a = FreeT { runFreeT :: m (FreeF f a (FreeT f m a)) }
data FreeF f a b = Pure a | Free (f b)
deriving Functor
```

Instances are left in the appendix.

The `FreeT`

type maps a functor `f :: * -> *`

to a monad transformer `FreeT f :: (* -> *) -> (* -> *)`

, and that mapping should be functorial. To define that functor, we must first spell out the categories defining the domain and codomain.

This will make `FreeT`

a functor between categories of functors, which is the kind of remark that makes category theory notoriously confusing.

### Domain and codomain

The domain is the category of functors `f :: * -> *`

and natural transformations; the codomain is a category of monad transformers, but it may seem unclear what its morphisms should be. We will try to describe the categorical structures of the domain and codomain in parallel.

A functor `f :: * -> *`

maps a type `a :: *`

to a type `f a :: *`

.

A monad transformer `t :: (* -> *) -> (* -> *)`

maps a monad `m :: * -> *`

to a monad `t m :: * -> *`

.

Types form a category, where morphisms are functions.

Monads form a category, where morphisms are monad morphisms.

A natural transformation `h :: f ~> g`

(a “functor morphism”) between two functors `f, g :: * -> *`

maps a type `a :: *`

to a function `h @a :: f a -> g a`

.

A monad transformer morphism `k :: t ~~> u`

between monad transformers `t, u :: (* -> *) -> (* -> *)`

maps a monad `m`

, to a monad morphism `k @m :: forall a. t m a -> u m a`

.

A natural transformation `h`

commutes with the functorial mapping `fmap`

.

`h @b . fmap @f = fmap @g . h @a`

A monad transformer morphism `k`

“commutes” with `lift`

.

`k @m . lift @t = lift @u`

### Mapping morphisms

To be a functor, `FreeT`

should map natural transformations `f ~> g`

to monad transformer morphisms `FreeT f ~~> FreeT g`

. This mapping is called `transFreeT`

in the `free`

library.

```
-- Only one of (Functor f) or (Functor g) is actually necessary for the
-- implementation.
transFreeT :: forall f g. Functor g => (f ~> g) -> (FreeT f ~~> FreeT g)
transFreeT h = FreeT . trans . runFreeT
where
trans :: forall m a. Monad m
=> m (FreeF f a (FreeT f m a))
-> m (FreeF g a (FreeT g m a))
trans = fmap @m (fmap @(FreeF g a) (transFreeT h) . transFreeF h)
transFreeF :: (f ~> g) -> (FreeF f a ~> FreeF g a)
transFreeF _ (Pure a) = Pure a
transFreeF h (Free f) = Free (h f)
```

And that mapping should preserve composition.

```
transFreeT id = id
transFreeT (h . i) = transFreeT h . transFreeT i
```

#### Semi-proof

For example, the left hand side of the first equation reduces to:

`transFreeT id = FreeT . fmap (transFreeT id) . runFreeT`

And there’s probably an argument (by induction?) to conclude from there.

`FreeT`

is a left adjoint

A free functor is a left adjoint to a forgetful functor.

Here, `FreeT`

maps a functor `f`

to a monad transformer `FreeT f`

. A corresponding “forgetful functor” should somehow map a monad transformer `t`

to a functor `Forget t`

. Let us find a good functor.

If we use `t`

to transform a well-chosen monad, then we get another monad, which is also a functor, exactly what we’re looking for. We shall choose the identity monad, as it is the most “neutral” of them in some sense. This may be abstractly motivated by the fact that it is the initial object in the category of monads and monad morphisms. It is most straightforwardly represented as a newtype:

But it will be a bit more convenient to use the following equivalent representation:

Then, the forgetful functor is obtained as:

We shall use the definition of adjoint functors by Hom isomorphism: there is a natural isomorphism between `f ~> Forget t`

and `FreeT f ~~> t`

. In particular, it consists of a bijection given by the following functions.

Imagine `f`

as specifying *elements of syntax*. The first direction means that if we can interpret these elements individually, then we can interpret an AST as a whole. This is `foldFreeT`

.

```
foldFreeT
:: (Functor f, MonadTrans t) => (f ~> Forget t) -> (FreeT f ~~> t)
foldFreeT h = k
where
k (FreeT m) = monadTrans $ lift m >>= \v -> case v of
Pure a -> return a
Free f -> h f >>= k
```

The other direction seems less useful; it says that every monad transformer morphism out of a free monad transformer can be decomposed as a `foldTreeT`

of some natural transformation, which is equivalent to a straightforward restriction of that morphism.

```
restrict :: Functor f => (FreeT f ~~> t) -> (f ~> Forget t)
restrict k = k . FreeT . return . Free . fmap return
```

The bijection we just gave is *natural*, making this diagram commute for all `k :: FreeT f ~~> t`

, `i :: g ~> f`

and `l :: t ~~> u`

,

```
. restrict
(FreeT f ~~> t) -> (f ~> Forget t)
| |
dimap i (forget l) | | dimap (transFreeT i) l
v restrict v
(FreeT g ~~> u) -> (g ~> Forget u)
-- or as an equation --
forget l . restrict k . i = restrict (l . k . transFreeT i)
```

where `forget`

is the forgetful functorial mapping:

and `dimap`

is a bifunctorial mapping:

This was a fun exercise in category theory. After figuring it out, I was surprised to see that `foldFreeT`

was not in `free`

, but now it is.