Skip to content

N_P3Ch08b_FalgFreeMonad

Jump to bottom
rpeszek edited this page Feb 22, 2018 · 4 revisions

Markdown of literate Haskell program. Program source: /src/CTNotes/P3Ch08b_FalgFreeMonad.lhs

Notes about CTFP Part 3 Chapter 8. F-Algebras. Free

Notes about F-algerbas and the free monad. The book does not talk about Free but I decided to research it and I wrote this note about it.

Book Ref: CTFP P3 Ch8. F-Algebras.

Refs: Doel, schoolofhaskell
comonad reader
nlab free monad

 module CTNotes.P3Ch08b_FalgFreeMonad where
 import Control.Monad

Free Monad

Free functor (free monad):

 data Free f a = Pure a | MkFree (f (Free f a))
 
 instance Functor f => Functor (Free f) where
   fmap fn (Pure a) = Pure (fn a)
   fmap fn (MkFree expr) = MkFree (fmap fn <$> expr)
 instance Functor f => Monad (Free f) where
   return = Pure
   Pure x >>= g = g x
   MkFree f >>= g = MkFree $ (>>= g) <$> f
 instance Functor f => Applicative (Free f) where
   pure  = return
   (<*>) = ap

There is category Mnd where objects are monads and morphisms are natural transformations that play nice with the monadic structure. This category can also be viewed as category of monoids in monoidal category of endofunctors with composition.
Endo is standard category of endofunctors. (See nlab free monad for more information.)

Forgetful functor:

U :: Mnd -> Endo
U (T, join, return) = T

Free functor

F :: Endo -> Mnd
F (Fx) = Free Fx

form an adjunction F -| U.

The adjunction says that monad morphisms (in Mnd) from Free F A to some other monad M correspond to natural transformations from F to M. Natural transformations are used in implementing interpreters for Free DSLs. TODO Is this a theoretical backing for that DSL approach?

Side note: As pointed out by the above comonad post
"The dual of substitution is redecoration"
(see also https://www.ioc.ee/~tarmo/papers/sfp01-book.pdf).

Think about fmap as substitution and join as renormalization.

m >>= f = join (fmap f m)

In Free join is not renormalizing!

 joinF :: Functor f => Free f (Free f a) -> Free f a
 joinF (Pure a) = a
 joinF (MkFree as) = MkFree (fmap joinF as)

"free monad is purely defined in terms of substitution".
End side note.

Free Monad Adjunction and F-algebras

For a fixed functor f, in pseudo-Haskell:

U:: F-Alg -> Hask
U (f, a, ev) = a  
 
F:: Hask -> F-Alg
F a = (f, Free f a, MkFree)

Hom ((f, Free f a, MkFree), (f, b, evb) ~=  a -> b

This adjunction viewed as isomorphism of homsets means that each function a -> b has a corresponding F-alg morphism from Free f a to b. This is done by using evb to collapse all layers in Free f.

 type FAlgebra f a = f a -> a

Following method is the essential part of isomorphism in the reverse direction

 iter :: Functor f => (f a -> a) -> Free f a -> a
 iter _ (Pure a) = a
 iter phi (MkFree m) = phi (iter phi <$> m)
 iso1 :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
 iso1 a2b evb freefa = iter evb (fmap a2b freefa)

 iso0 :: (Free f a -> b) -> a -> b
 iso0 f = f . Pure

More about Free
The comonad post linked above continues as a 3 part sequel, N_P3Ch11a_KanExt has all of these posts linked.

Cofree

This section is mostly a TODO. Documentation in free package has good short description of Cofree.
https://hackage.haskell.org/package/free-5/docs/Control-Comonad-Cofree.html

Cofree and Free work together well. I have used it in my GraphPlay project. (TODO find good writeup)
See http://blog.sigfpe.com/2014/05/cofree-meets-free.html

Clone this wiki locally