Free monad

category: $\mathcal{S} : \text{has binary coproducts}$
endofunctor: $F : \mathcal{S} \rightarrow \mathcal{S}$
forgetful functor: $U : F \unicode{x2012} \mathcal{Alg} \rightarrow \mathcal{S}$

について、initial algebraの族:

$\big( \langle \mathtt{pure}_ a, \mathtt{free} _ a \rangle : a + F(\mathtt{Free} _ a) \rightarrow \mathtt{Free} _ a \big) _ {a \in \mathcal{S} }$

が存在するならば、Initial algebras with parameters - PSより、これをnaturalにするfunctor:

を作ることが出来る。いま、

とすると

は、initial morphismの族となるので

逆に、unit-adjunction:

が存在すれば、

は、initial algebraの族となる。

は、monadになる。*1

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

Initial algebraからのcatamorphism*2は、

cata :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
cata h phi (Pure a) = h a
cata h phi (Free m) = phi (fmap (cata h phi) m)

で、これから全て導かれる(はず)。

Adjunctionのunitは、constructorPureで、counitはiterになる(と思う)。

*1:Free monadの数学的定義はややこしい模様: Category of monads - PS

*2:mediatorのこと