Inductive type

関数 $f$ について、fixed pointとは、

を満たす $x$ のこと。これをendofunctorに拡張する。

Endofunctor $F$ について、 fixed pointとは、

を満たす $(A, a)$ のこと。

$F \unicode{x2013} \mathcal{Alg}$ のinitial objectのこと。

証明は簡単。

Initial algebraはleast fixed pointと考えられる。これでinductive typeを定義できる。たとえば、

から、 $\text{List} _ a \in \mathcal{Hask} _ 0$ を次のように定義できる。

$(\text{List} _ a, (\text{Nil} _ a, \text{Cons} _ a)) := \text{initial algebra of } F _ a$

Initial algebraの存在の証明は手間がかかる(模様)。

Initial algebraのmediating morphismのこと。

$\text{foldr} _ a (f) := \langle f \rangle _ { (\text{List}_a, (\text{Nil}_a, \text{Cons}_a) ) }$ *1
$\text{sum} := \text{foldr} _ {\text{Int}}(\text{Int}, ( \text{const}(0), \text{+}) )$

*1:mediating morphismの取り出し