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 #-}To make things unambiguous I'll implement free monads in the usual way here:
> import Control.Monad > import Data.Monoid
> data Free f a = Pure a | Free (f (Free 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.
> 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 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 aSo now we are led to consider functors in Endo.
> class HFunctor f whereA 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 bBut 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)(Compare with what I wrote here.)
> 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
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 awe 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 NilAnother 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:
> hsingleton :: Natural f (Free f) > hsingleton f = Free (fmap Pure f)
> 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)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.
> 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
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)We can define HMonad as follows:
> instance HFunctor Free where > ffmap = fmap > hfmap f = hFoldMap (hsingleton . f)
> 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 aBefore 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.
6 Comments:
There's a similar trick for Prompt, the free monad for a type constructor.
There's a similar trick for Prompt, the free monad for a unary type constructor.
Whats that :< symbol in the liked source mean?
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.
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.
The current closest thing to a home for HMonad and HFunctor is probably index-core by Gabriel Gonzales.
http://hackage.haskell.org/package/index-core-1.0.1/docs/Control-IMonad-Core.html
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.
https://github.com/ekmett/indexed
Post a Comment
<< Home