100年ぶりにポエムを書きます。
F代数から出発して、最終的にはCatamorphismを理解することを目指します。
F代数
ある関手Fに対して、対象と射の組 $(A, a : F(A) \rightarrow A)$ のこと。
\begin{CD}
F(A) @>a>> A
\end{CD}
Haskellで書くと、
type Algebra f a = f a -> a
F代数の準同型
ある2つのF代数 $(A, a)$, $(B, b)$ に対して、 $f \circ a = b \circ F(f)$ を満たす射 $f : A \rightarrow B$ のこと。
\begin{CD}
F(A) @>a>> A \\
@VF(f)VV @VfVV \\
F(B) @>b>> B
\end{CD}
F始代数
任意のF代数 $(X, \varphi)$ への準同型が一意に定まる特別なF代数。F始代数の対象を特に始対象と呼ぶ。
ここで、$(I, i)$ がF始代数であるならば、 $I \simeq F(I) $ ということが知られている1。つまり、任意のF代数 $(X, \varphi)$ に対して以下の可換図式が成り立つ。
\begin{CD}
F(I) @>i>> I \\
@VF(f)VV @VfVV \\
F(X) @>\varphi>> X
\end{CD}
Haskellで書くと、
newtype Fix f = InF { outF :: f (Fix f) }
Fix fが始対象$I$に, inFが可換図式の射 $i : F(I) \rightarrow I$ に相当する。outF は $i$ の逆射 $i^{-1} : I \rightarrow F(I)$ である。
名前の由来は $I$ が関手$F$の最小不動点であることから。
Catamorphism
上の可換図式で、射 $f$ はF始代数から任意のF代数 $(X, \varphi)$ への準同型である。これをCatamorphismと呼ぶことにする。
関手 $F$ におけるF始対象が関手 $F$の 不動点であることを強調するために、上図 $I$ を $Fix(F)$ に置き換えた図を示す。
\begin{CD}
F(Fix(F)) @>inF>> Fix(F) \\
@VF(cata(\varphi))VV @Vcata(\varphi)VV \\
F(X) @>\varphi>> X
\end{CD}
Haskellで書くと、
cata :: Functor f => (f a -> a) -> Fix f -> a
cata phi = phi . fmap (cata phi) . outF
phi :: Functor f => f a -> aが可換図式の $\varphi$に相当する。あるいは、F代数で紹介したAlgebraを使って、
type Algebra f a = f a -> a
cata :: Functor f => Algebra f a -> Fix f -> a
cata phi = phi . fmap (cata phi) . outF
と書いてもいいかもしれない。こちらの方が、cataが任意のF代数 $(X, \varphi)$ を得てF始対象から$X$への準同型$cata(\varphi)$を返す様子がよくわかる。
Haskellの実装は、可換図式を左側からぐるっと回り込むようなイメージでされている。
outFは $inF$ の逆射で、F始代数の性質 $Fix(F) \simeq F(Fix(F)) $ より得られる。
\begin{CD}
cata(\varphi) = Fix(F) @>inF^{-1}>> F(Fix(F)) @>F(cata(\varphi))>> F(X) @>\varphi>> X
\end{CD}
プログラミングにおける意義
プログラミングにおいて、Catamorphismは畳み込み処理の一般化といえる。
Fix fが何らかの再帰的構造を表している（Fix f = f (Fix f) = f (f (Fix f))）ことから、cataの型のFix f -> aの部分はある再帰的構造をある一つの値に畳み込むことを示していると解釈できる。
cataの型を再掲しよう。
cata :: Functor f => Algebra f a -> Fix f -> a
具体例を考えてみる。
$ListF_X = 1 + X \times Y$という関手の不動点 $Fix (ListF_X)$ は、リスト $List(X)$ と同型である。
ところで、Haskellにはリストの畳み込み処理をする関数foldrがある。この $ListF_X$ をcataの型に当てはめてみれば、得られる関数は foldrと同等のものであるはずである。
-- ListFx = 1 + X * Y
data ListF a b = Nil | Cons a b deriving (Functor)
-- ListFで特殊化したcata
cata :: (ListF a b -> b) -> Fix (ListF a) -> b
foldrの型を確認しよう。
foldr :: (a -> b -> b) -> b -> [a] -> b
おや、cataとfoldrの型が違ってしまっている。これはどうしたことだろう。
cataの型を同型を使って変形していき、最終的にfoldrの型が得られることを確認しよう。
-
Fix (ListF a) ~= [a]
まずは、$ListF_X$の不動点がリスト$List$と同型であるので、そこから置き換えていく。cata :: (ListF a b -> b) -> [a] -> b -
(ListF a b -> b) ~= (Maybe (a, b) -> b)
$ListF_X = 1 + X \times Y$ だった。
(a, b)が $X \times Y$ 、Maybe aが $1 + X$ と対応する。cata :: (Maybe (a, b) -> b) -> [a] -> b -
(Maybe (a, b) -> b) ~= ((a, b) -> b, b)
ゴチャとしてるけど、(Maybe a -> b) ~= (a -> b, b)というだけ。cata :: ((a, b) -> b, b) -> [a] -> b -
((a, b) -> b) ~= a -> b -> b
(a, b) -> c ~= a -> b -> c
つまりカリー化。cata :: (a -> b -> b, b) -> [a] -> b -
(a -> b -> b, b) ~= (a -> b -> b) -> b
カリー化二回目。cata :: (a -> b -> b) -> b -> [a] -> b
できた。
まとめ
F代数を学ぶところから出発して、F始対象が関手$F$の不動点であることに注意しながら、F始代数から任意のF代数への準同型であるCatamorphismがプログラミングの畳み込み処理と深く関連していることを確認した。
おじいさん、明日のご飯はAnamorphismですよ。