Friday, April 25, 2014

The Monad called Free


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.


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.


Blogger Dave Menendez said...

There's a similar trick for Prompt, the free monad for a type constructor.

Friday, 25 April, 2014  
Blogger Dave Menendez said...

There's a similar trick for Prompt, the free monad for a unary type constructor.

Friday, 25 April, 2014  
Blogger Yukarin-chan said...

Whats that :< symbol in the liked source mean?

Saturday, 26 April, 2014  
Blogger Unknown said...

Slight typo, where it says "the category of endomorphisms", it should say "the category of endofunctors", where the objects are endofunctors and the morphisms are natural transformations.

Saturday, 26 April, 2014  
Blogger Edward Kmett said...

What you are looking for is the free package on hackage.

Control.Monad.Free is there alongside free Applicatives and Alternatives and other encodings of the free monad and free monad transformer.

Saturday, 26 April, 2014  
Blogger Edward Kmett said...

The current closest thing to a home for HMonad and HFunctor is probably index-core by Gabriel Gonzales.

I have work partially done on a replacement for indexed, but it is currently hung up waiting for GHC to fix Any so that it doesn't inhabit every kind, so we can have proper product kinds.

Saturday, 26 April, 2014  

Post a Comment

<< Home