List
／＼
a1 ／＼
a2 ／＼
a3 nil
foldr
f
／＼
a1 f
／＼
a2 f
／＼
a3 zero
似ている*2。
foldrの最も汎用的な形がList*4。
↓
foldrの始対象がList*5。
↓
ListはF代数の圏におけるF始代数*6
List foldr f
／＼ ／＼
a1 ／＼ <------ 抽象的 ------ a1 f
a2 ／＼ - 関数(射)が作れそう-> ／＼
a3 nil a2 f
／＼
a3 zero
List
cons
／＼
a1 cons
／＼
a2 cons
／＼
a3 nil
foldr
f
／＼
a1 f
／＼
a2 f
／＼
a3 zero
似ている*2。
foldrの最も汎用的な形がList*4。
↓
foldrの始対象がList*5。
↓
ListはF代数の圏におけるF始代数*6
List cons foldr f
／＼ ／＼
a1 cons <------ 抽象的 ------ a1 f
／＼ - 関数(射)が作れそう-> ／＼
a2 cons a2 f
／＼ ／＼
a3 nil a3 zero
f: A * Y -> Y g: A * Z -> Z
∮ = foldr f zero
X = List<A> ---------------------------> F<X> = Y
ex) cons(a1, cons(a2, cons(a3, nil))) ex) f(a1, f(a2, f(a3, zero))) = y
id ↓ ↓ τ: F<X> -> G<X> = Y -> Z
γ = foldr g zero
X = List<X> ---------------------------> G<X> = Z
ex) cons(a1, cons(a2, cons(a3, nil))) ex) g(a1, g(a2, g(a3, zero))) = z
∮
Ｘ----->Ｙ
＼ ｜
γ ＼ ｜ τ
＼ ↓
Ｚ
τ・∮ = γ である τ を考えることができる…？