Kleisli Categories and Free Monads

Given a monad m one can construct the Kleisli category Control.Arrow.Kleisli m, in this post we’ll explore what happens when we start with a free monad.

Kleisli contstruction

The Keisli composition is so useful, it has it’s own operator defined in Control.Monad:

Free monads

Free monad construction gives you a monad out of a functor. It will satisfy all the monad laws: associativity, and unitality axioms, and it is a universal construction.

The universal property of a free monad can be expressed with a class, which I borrowed from free-algebras package (I don’t include all details that are not important for this blog post; The details where described in this post):

In this blog post whenever we will refer to liftFree and foldNatFree we will actually refer to this instance:

You probably recognise Free.liftF and Free.foldFree from the free package.

Instances of this class have the property that to construct a natural transformation from FreeAlgebra1 m => m f to a monad Monad d => d is enought to come up with a natural transformation of functors forall x. f a -> d a. If you’d like to explore more why this class is the right one to speak about freeness, checkout one of my previous posts. Note that the instance for Free follows the structure, and there is no room how to implement the methods: that’s a very common feeling in category theory, which means one is on the right path.

This particular instance satisfies rather interesting laws:

liftFree natural transformation
liftFree natural transformation

or as an equation:

fmap g . liftFree == liftFree . fmap g

This is more or less streightforward, just take a look at the definition of liftFree.

foldNatFree natural transformation
foldNatFree natural transformation

or as an equation:

fmap g . foldNatFree nat == foldNatFree nat . fmap g

This one is slightly more involved, and lets prove it:

(foldNatFree nat . fmap g) (Return a)
  = foldNatFree nat (Return (g a))
  = return (g a)
  = fmap g (return a)
  = fmap g (foldNatFree nat (Return a))
  = (fmap g . foldNatFree nat) (Return a)

and

(foldNatFree nat . fmap g) (Free ff)
  = foldNatFree nat (fmap g (Free ff))
  = foldNatFree nat (Free (fmap (fmap g) ff))
  = join $ nat $ foldNatFree nat <$> (fmap (fmap g) ff)
  = join $ nat $ foldNatFree nat <$> fmap g <$> ff
  = join $ nat $ (foldNatFree nat . fmap g) <$> ff
  -- by induction hypotesis
  = join $ nat $ (fmap g . foldNatFree nat) <$> ff
  = join $ nat $ fmap g <$> (foldNatFree nat <$> ff)
  = join $ nat $ fmap (fmap g) (foldNatFree nat <$> ff)
  -- since nat is a natural transformation
  = join $ fmap (fmap g) $ nat (foldNatFree nat <$> ff)
  -- join is a natural transformation
  -- join :: Monad m => m (m a) -> m a
  = fmap g $ join $ $ nat (foldNatFree nat <$<> ff)
  = fmap g $ foldNatFree nat (Free ff)
  = (fmpg g . foldNatFree nat) (Free ff)

Since in our case Free is a functor from the category of (endo-)functors into the category of monads. foldNatFree nat has to ba monad morphism for any nat. This means that the following diagrams commute (or equations hold):

foldNatFree - monad morphism: the unit law
foldNatFree - monad morphism: the unit law

or as an equation:

return = return . foldNatFree nat

This should be clear from definition of foldNatFree. Moreover, the following diagram commutes:

foldNatFree - monad morphism: the join law
foldNatFree - monad morphism: the join law

or as an equation:

join . (foldNatFree nat . fmap (foldNatFree nat))
  == foldNatFree nat . join

Let us prove this it:

join . (foldNatFree nat . fmap (foldNatFree nat)) (Return (Return a))
  == join (foldNatFree nat (Return (foldNatFree nat (Retrun a))))
  == join (foldNatFree nat (Return (return a))
  == join (return (return a))
  == return a
  == foldNatFree nat (Return a)
  == foldNatFree nat (join (Return (Return a)))

And the other one, which we prove starting from the right hand side:

foldNatFree nat (join (Free ff)))
  -- by definition of join
  = foldNatFree nat (Free (fmap join ff))
  -- by definition of foldNatFree
  = join $ nat $ fmap (foldNatFree nat) (fmap join ff)
  = join $ nat $ fmap (foldNatFree nat . join) ff
  -- by induction hypotesis
  = join $ nat $ fmap (join . foldNatFree nat . fmap (foldNatFree nat)) ff
  = join $ nat $ fmap join $ fmap (foldNatFree nat) $
      fmap (fmap foldNatFree nat)) ff
  -- since nat is a natural transformation
  = join $ fmap join $ nat $ fmap (foldNatFree nat) $
      fmap (fmap (foldNatFree nat)) ff
  -- by associativity of join
  = join $ join $ nat $ fmap (foldNatFree nat) $
      fmap (fmap (foldNatFree nat)) ff
  -- by definition of foldNatFree (the outer one)
  = join $ foldNatFree nat $ Free $ fmap (fmap (foldNatFree nat)) ff
  -- by definition of functor instance for Free
  = join $ foldNatFree nat $ fmap (foldNatFree nat) $ Free ff
  = (join . foldNatFree nat . fmap (foldNatFree nat)) $ Free ff

Note that by the natural transformation law for foldNatFree we have:

foldNatFree nat . fmap (foldNatFree nat)
  == fmap (foldNatFree nat) . foldNatFree nat

For any monad morphism fn :: (Monad m, Monad n) => m a -> n a, we will show that:

fn . (f <=< g) == (fn . f) <=< (fn . g)

in particular this is true for foldNatFree nat.

(fn . f <=< fn . g)
  == \a -> fn . f =<< (fn . g) a
  == \a -> fn . f =<< fn (g a)
  -- by definition of join (or =<< in terms of a join)
  == \a -> join (fn . f <$> fn (g a))
  -- by functor associativity law
  == \a -> join (fn <$> (f <$> fn (g a)))
  -- since fn is a morphism of monads it is a natural transformation
  -- and thus it commutes with fmap/<$>
  == \a -> join (fn <$> (fn (f <$> g a)))
  -- since fn is a morphism of monads: join (fmap fn . fn) == fn . join
  == \a -> fn (join (f <$> g a))
  -- by definition of join
  == \a -> fn (f =<< g a)
  == \a -> fn (f <=< g) a
  == fn (f <=< g)

The proof could be much shorter if we use monad morphism law in terms of binds. The equivalne form of join (fmap fn . fn) == fn . join expressed with bind is fn (f =<< ma) = (fn . f) =<< fn ma. A reason to use join is that the law take the same form as for monoid homomorphisms, so it is very easy to remember them.

Kleisli categories for free monads

This means that Kleisli (Free f) is a free category for the class of graphs of type

Functor f => Kleisli f

(Keisli f is a category only when f is a monad). Both morphisms: liftKleisli is marely a morphisms of graphs, while foldKleisli is a functor, which means it preserves id and the composition (.) :: Category c => c y z -> c x y -> c x y.

foldKleisli nat id
  == foldKleisli nat (Kleisli Return)
  == Kleisli (foldNatFree nat . Return)
  == Kleisli return
  == id
foldKleisli nat (Kleisli f . Kleisli g)
  == foldKleisli nat (Kleisli f <=< g)
  == Kleisli (foldNatFree nat (f <=< g))
  -- foldNatFree nat is a morphism of monads thus
  == Kleisli (foldNatFree nat f <=< foldNatFree nat g)
  == Kleisli (foldNatFree nat f) . Kleisli (foldNatFree nat g)
  == foldKleisli nat f . foldKleisli nat g