$\require{AMScd}$
はじめに
Haskellを勉強していると諸々の概念と圏論の繋りが気になってきます。今回は代数的データ型について圏論との関係を述べます。
なお、面倒なので圏と関手、直積、直和はわかっているものとして話しを進めます。
F代数
自己関手$F : C \to C$について$F$代数とは$C$の対象$A$と$C$の射$a : F(A) \to A$の組$(A, a)$のことです。このとき$F$代数$(A, a)$と$(B, b)$の間の射とは$C$の射$f : A \to B$であり、以下の図を可換にするものである。
\begin{CD}
F(A) @>F(f)>> F(B) \\
@VaVV @VbVV \\
A @>f>> B
\end{CD}
この対象と射により$F$代数は圏を成します。 この$F$代数の圏における始対象を$F$始代数と呼びます。
Lambekの定理
$F$始代数$\alpha = (A, a)$について以下が成り立つ。
$$
F(A) \cong A
$$
$(F(A), F(a))$は$F$代数である。このとき$\alpha$が始対象であることから、以下の図を可換にする射$i$が唯一存在する。
\begin{CD}
F(A) @>F(i)>> F(F(A)) \\
@VaVV @VF(a)VV \\
A @>i>> F(A)
\end{CD}
この$i$が$a$の逆射であることを示す。$a \circ i$は$\alpha$の自己準同型であり、$\alpha$は始対象であるので$a \circ i = {\rm id}$となる(以下の図を参照)。
\begin{CD}
F(A) @>F(i)>> F(F(A)) @>F(a)>> F(A) \\
@VaVV @VF(a)VV @VaVV \\
A @>i>> F(A) @>a>> A
\end{CD}
次に$i \circ a$を考える。
\begin{array}{lcl}
i \circ a &=& F(a) \circ F(i) \\
&=& F(a \circ i) \\
&=& F({\rm id}) \\
&=& {\rm id} \\
\end{array}
よって$i = \alpha^{-1}$となり$F(A) \cong A$。
リストによる具体例
関手$F(X) = 1 + B \times X$の$F$始代数$(A, a)$が存在したとするとLambekの定理から$F(A) \cong A$となり、これを展開すると以下の式ができる。
$$
A \cong 1 + B \times A
$$
この$A$を${\rm List}\ B$で置き換えてみる。
$$
{\rm List}\ B \cong 1 + B \times {\rm List}\ B
$$
これはリストの定義に他ならない。
data List b = Nil
| Cons b (List b)
ここで$a : 1 + B \times A \to A$なので$n : 1 \to A$と$c : B \times A \to A$を用いて$a = [n, c]$と表わせる。この$n, c$はそれぞれリストにおけるNilとConsに対応する。また、$(A, a)$が始対象であることから任意の$F$代数$(X, \phi)$への射$|\phi|$が唯一存在し、以下の図を可換にする。
\begin{CD}
1+B\times A @>F(|\phi|)>> 1+B\times X \\
@V[n, c]VV @V\phi VV \\
A @>|\phi|>> X \\
\end{CD}
ここで$a$のときと同様に$\phi = [x, f]$と表わせる。
\begin{CD}
1+B\times A @>1+B\times|[x, f]|>> 1+B\times X \\
@V[n, c]VV @V[x, f] VV \\
A @>|[x, f]|>> X \\
\end{CD}
この図から直和の性質を用いて2つの図に分解する。
\begin{CD}
1 @>{\rm id}>> 1 \\
@VnVV @VxVV \\
A @>|[x, f]|>> X
\end{CD}
\begin{CD}
B\times X @<B\times|[x,f]|<< B\times A \\
@VfVV @VcVV \\
X @<|[x,f]|<< A
\end{CD}
この図から以下の2つの等式が導ける。
\begin{array}{lcl}
|[x,f]|\circ n &=& x \\
|[x,f]|\circ c &=& f \circ (B \times |[x, f]|)
\end{array}
これはfoldrの定義に他ならない。
foldr :: a -> (b -> a -> a) -> List b -> a
(foldr x f) Nil = x
(foldr x f) (Cons a as) = f a ((foldr x f) as)
すなわち$F$始代数からの射は畳み込み(fold)に対応し、この射はcatamorphismと呼ばれる。畳み込みがcatamorphismであること、すなわち始対象からの射であることから畳み込みの融合則などが導かれる。
代数的データ型とは単なるF始代数だよ
何か問題でも?
代数的データ型は単なるF始代数と言ったな、あれは嘘だ。
$F$始代数には双対概念である$F$終余代数が存在します。$F$始代数は有限のデータ構造を表わすのに対して、$F$終余代数は無限のデータ構造を表わします。話しをHaskellに限定するとHaskellは遅延評価を採用しているため、代数的データ型で無限のデータ構造を表現でき、$F$始代数と$F$終余代数が一致します。
catamorphismの双対はanamorphismと呼ばれ、catamorphismが$F$始代数の値を消費するのに対して、anamorphismは$F$終余代数の値を構築します。このように畳み込みと逆の性質を持っているため、Haskellではunfoldという名前で定義されています。興味がある方はこれらのキーワードで調べて下さい。私は終余代数はよくわかりません。
参考文献
今回は$F$代数の定義から始めてトップダウンに代数的データ型の意味を説明しましたが、圏論勉強会の資料では自然数の表し方からボトムアップに代数的データ型に$F$始代数としての意味を与えています。また、$F$始代数が存在する条件など更に進んだ内容も述べられているので詳しく学びたい人は読むべきでしょう。
- Lambekの定理の証明 Lambek's theorem
- F代数 - Wikipedia
- 圏論勉強会第7回
- 圏論勉強会第8回
- 圏論勉強会第10回