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.

type f ~> g = forall 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.

type t ~~> u = forall m a. Monad m => 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:

newtype Identity' a = Identity' a

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

type Identity a = forall m. Monad m => m a

Then, the forgetful functor is obtained as:

type Forget t a = forall m. Monad m => t m a

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:

forget :: (t ~~> u) -> (Forget t ~> Forget u)
forget k = k

and dimap is a bifunctorial mapping:

dimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d)
dimap i l k = l . k . i

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.

Appendix

instance (Functor f, Monad m) => Functor (FreeT f m) where
  fmap = liftM

instance (Functor f, Monad m) => Applicative (FreeT f m) where
  pure = return
  (<*>) = ap

instance (Functor f, Monad m) => Monad (FreeT f m) where
  return = FreeT . return . Pure
  FreeT m >>= f = FreeT $ m >>= \v -> case v of
    Pure a -> runFreeT (f a)
    Free w -> return (Free (fmap (>>= f) w))

instance Functor f => MonadTrans (FreeT f) where
  lift = FreeT . fmap Pure
  monadTrans t = t