Free monad and the free operation

One way to describe the Free monad is to say it is an initial monoid in the category of endofunctors (of some category C ) whose objects are the endofunctors from C to C , arrows are the natural transformations between them. If we take C to be Hask , the endofunctor are what is called Functor in haskell, which are functor from * -> * where * represents the objects of Hask

By initiality, any map from an endofunctor t to a monoid m in End(Hask) induces a map from Free t to m .

Said otherwise, any natural transformation from a Functor t to a Monad m induces a natural transformation from Free t to m

I would have expected to be able to write a function

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta) 

but this fails to unify, whereas the following works

free :: (Functor t, Monad m) => (t (m a) → m a) → (Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

or its generalization with signature

free :: (Functor t, Monad m) => (∀ a. t a → a) → (∀ a. Free t a → m a)

Did I make a mistake in the category theory, or in the translation to Haskell ?

I'd be interested to hear about some wisdom here..

PS : code with that enabled

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
import Control.Monad.Free

---

The Haskell translation seems wrong. A big hint is that your free implementation doesn't use monadic bind (or join) anywhere. You can find free as foldFree with the following definition:

free :: Monad m => (forall x. t x -> m x) -> (forall a. Free t a -> m a)
free f (Pure a)  = return a
free f (Free fs) = f fs >>= free f

The key point is that f specializes to t (Free ta) -> m (Free ta) , thus eliminating one Free layer in one fell swoop.

---

I don't know about the category theory part, but the Haskell part is definitely not well-typed with your original implementation and original type signature.

Given

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)

when you pattern match on Free tfta , you get

tfta :: t (Free t a)
f :: forall a. t a -> m a 
free :: (forall a. t a -> m a) -> forall a. Free t a -> m a

And thus

free f :: forall a. Free t a -> m a

leading to

fmap (free f) :: forall a. t (Free t a) -> t (m a) 

So to be able to collapse that t (ma) into your desired ma , you need to apply f on it (to "turn the t into an m ") and then exploit the fact that m is a Monad:

f . fmap (free f) :: forall a. t (Free t a) -> m (m a)
join . f . fmap (free f) :: forall a. t (Free t a) -> m a

which means you can fix your original definition by changing the second branch of free :

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

import Control.Monad.Free
import Control.Monad

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free tfta) = join . f . fmap (free f) $ tfta

This typechecks, and is probably maybe could be what you want :)

链接地址: http://www.djcxy.com/p/47700.html

上一篇: 什么是函数式编程？

下一篇: 免费的monad和免费的操作