A Neighborhood of Infinity: The Monad called Free

Introduction

As Dan Doel points out here, the gadget Free that turns a functor into a monad is itself a kind of monad, though not the usual kind of monad we find in Haskell. I'll call it a higher order monad and you can find a type class corresponding to this in various places including an old version of Ed Kmett's category-extras. I'll borrow some code from there. I hunted around and couldn't find an implementation of Free as an instance of this class so I thought I'd plug the gap.

> {-# LANGUAGE RankNTypes, FlexibleContexts, InstanceSigs, ScopedTypeVariables #-}


> import Control.Monad
> import Data.Monoid

To make things unambiguous I'll implement free monads in the usual way here:

> data Free f a = Pure a | Free (f (Free f a))


> instance Functor f => Functor (Free f) where
>     fmap f (Pure a) = Pure (f a)
>     fmap f (Free a) = Free (fmap (fmap f) a)


> instance Functor f => Monad (Free f) where
>     return = Pure
>     Pure a >>= f = f a
>     Free a >>= f = Free (fmap (>>= f) a)

The usual Haskell typeclass

Monad

corresponds to monads in the category of types and functions,

Hask

. We're going to want monads in the category of endomorphisms of

Hask

which I'll call

Endo

.

The objects in Endo correspond to Haskell's Functor. The arrows in Endo are the natural transformations between these functors:

> type Natural f g = (Functor f, Functor g) => forall a. f a -> g a

So now we are led to consider functors in

Endo

.

> class HFunctor f where

A functor in

Endo

must map functors in

Hask

to functors in

Hask

. So if

f

is a functor in

Endo

and

g

is a functor in

Hask

, then

f g

must be another functor in

Hask

. So there must be an

fmap

associated with this new functor. There's an associated

fmap

for every

g

and we collect them all into one big happy natural family:

>     ffmap :: Functor g => (a -> b) -> f g a -> f g b

But note also that by virtue of being a functor itself,

f

must have its own

fmap

type function associated with it. The arrows in

Endo

are natural transformations in

Hask

so the

fmap

for

HFunctor

must take arrows in

Endo

to arrows in

Endo

like so:

>     hfmap :: (Functor g, Functor h) => Natural g h -> Natural (f g) (f h)

Many constructions in the category

Hask

carry over to

Endo

. In

Hask

we can form a product of type types

a

and

b

as

(a, b)

. In

Endo

we form the product of two functors

f

and

g

as

> data Product f g a = Product (f (g a))

Note that this product isn't commutative. We don't necessarily have an isomorphism from

Product f g

to

Product g f

. (This breaks many attempts to transfer constructions from

Hask

to

Endo

.) We also won't explicitly use

Product

because we can simply use the usual Haskell composition of functors inline.

We can implement some functions that act on product types in both senses of the word "product":

> left :: (a -> c) -> (a, b) -> (c, b)
> left f (a, b) = (f a, b)


> right :: (b -> c) -> (a, b) -> (a, c)
> right f (a, b) = (a, f b)


> hleft :: (Functor a, Functor b, Functor c) => Natural a c -> a (b x) -> c (b x)
> hleft f = f


> hright :: (Functor a, Functor b, Functor c) => Natural b c -> a (b x) -> a (c x)
> hright f = fmap f

(Compare with what I wrote here.)

We have something in Endo a bit like the type with one element in Hask, namely the identity functor. The product of a type a with the one element type in Hask gives you something isomorphic to a. In Endo the product is composition for which the identity functor is the identity. (Two different meanings of the word "identity" there.)

We also have sums. For example, if we define a functor like so

> data F a = A a | B a a

we can think of

F

as a sum of two functors: one with a single constructor

A

and another with constructor

B

.

We can now think about reproducing an Endo flavoured version of lists. The usual definition is isomorphic to:

> data List a = Nil | Cons a (List a)

And it has a

Monoid

instance:

> instance Monoid (List a) where
>   mempty = Nil
>   mappend Nil as = as
>   mappend (Cons a as) bs = Cons a (mappend as bs)

We can try to translate that into

Endo

. The

Nil

part can be thought of as being an element of a type with one element so it should become the identity functor. The

Cons a (List a)

part is a product of

a

and

List a

so that should get replaced by a composition. So we expect to see something vaguely like:

List' a = Nil' | Cons' (a (List' a))

That's not quite right because

List' a

is a functor, not a type, and so acts on types. So a better definition would be:

List' a b = Nil' b | Cons' (a (List' a b))

That's just the definition of

Free

. So free monads are lists in

Endo

. As everyone knows :-) monads are just monoids in the category of endofunctors. Free monads are also just free monoids in the category of endofunctors.

So now we can expect many constructions associated with monoids and lists to carry over to monads and free monads.

An obvious one is the generalization of the singleton map a -> List a:

> singleton :: a -> List a
> singleton a = Cons a Nil


> hsingleton :: Natural f (Free f)
> hsingleton f = Free (fmap Pure f)

Another is the generalization of

foldMap

. This can be found under a variety of names in the various free monad libraries out there but this implementation is designed to highlight the similarity between monoids and monads:

> foldMap :: Monoid m => (a -> m) -> List a -> m
> foldMap _ Nil = mempty
> foldMap f (Cons a as) = uncurry mappend $ left f $ right (foldMap f) (a, as)


> fold :: Monoid m => List m -> m
> fold = foldMap id


> hFoldMap :: (Functor f, Functor m, Monad m) => Natural f m -> Natural (Free f) m
> hFoldMap _ (Pure x) = return x
> hFoldMap f (Free x) = join $ hleft f $ hright (hFoldMap f) x


> hFold :: Monad f => Natural (Free f) f
> hFold = hFoldMap id

The similarity here isn't simply formal. If you think of a list as a sequence of instructions then

foldMap

interprets the sequence of instructions like a computer program. Similarly

hFoldMap

can be used to interpret programs for which the free monad provides an abstract syntax tree.

You'll find some of these functions here by different names.

Now we can consider Free. It's easy to show this is a HFunctor by copying a suitable definition for List:

> instance Functor List where
>   fmap f = foldMap (singleton . f)


> instance HFunctor Free where
>     ffmap = fmap
>     hfmap f = hFoldMap (hsingleton . f)

We can define

HMonad

as follows:

> class HMonad m where
>     hreturn :: Functor f => f a -> m f a
>     hbind :: (Functor f, Functor g) => m f a -> Natural f (m g) -> m g a

Before making

Free

an instance, let's look at how we'd make

List

an instance of

Monad

> instance Monad List where
>     return = singleton
>     m >>= f = fold (fmap f m)

And now the instance I promised at the beginning.

> instance HMonad Free where
>     hreturn = hsingleton
>     hbind m f = hFold (hfmap f m)

I've skipped the proofs that the monad laws hold and that

hreturn

and

hbind

are actually natural transformations in

Endo

. Maybe I'll leave those as exercises for the reader.

Update

After writing this I tried googling for "instance HMonad Free" and I found this by haasn. There's some other good stuff in there too.