PS

fold/build fusion

圏論命題 F-algebra Haskell

命題

endofunctor: $F : \mathcal{C} \to \mathcal{C}$
forgetful functor: $U: \operatorname{\mathit{F}-\mathcal{Alg}} \to \mathcal{C}$

について、initial algebra:

$\mathtt{in} : F(\mu F) \to \mu F$

が存在するならば、そのcatamorphimの族:

$\big( \mathtt{fold}(h) : \mu F \to U(h) \big) _ { h \in \operatorname{\mathit{F}-\mathcal{Alg}} }$

は、mediatorを

$\mathtt{build}(\sigma : \Delta C \Rightarrow U) := \sigma _ { \mathtt{in} } : C \to \mu F$

とする limiting cone of $U$ になる:

$\mathtt{fold}(h) \circ \mathtt{build}(\sigma) = \sigma _ h$ 　(fold/build fusion)

参考文献

Initial algebra semantics is enough