最近よく耳にするFreeモナドについて、自分用にまとめました。自分以外にはわかりづらい可能性があります。
モナドとは
自己関手の圏 $\mathcal{C}\to\mathcal{C}$ におけるモノイドのことです。
つまり関手 $M\colon\mathcal{C}\to\mathcal{C}$ で積 $M^2\to M$ と単位 $\mathrm{Id}\to M$ が与えられていて結合律と単位律を満たすもの。
Freeモナドとは
関手 $F\colon\mathcal{C}\to\mathcal{C}$ に対し、文字通り $F$ で生成される自由なモナドのこと。
つまりモナド $F^*\colon\mathcal{C}\to\mathcal{C}$ と関手の射 $F\to F^*$ の組であって、別のモナド $M\colon\mathcal{C}\to\mathcal{C}$ と関手の射 $F\to M$ があったらそれが一意的にモナドの射 $F^*\to M$ を経由するようなもの。
性質
$F$ のFreeモナド $F^*$ が存在するとする。すると自然に次のような同型がある。
$$F^* = \mathrm{Id} + FF^*$$
まず右辺から左辺への射は $F^*$ の積と単位を使って $FF^*\to F^*F^*\to F^*$ と $\mathrm{Id}\to F^*$ から作ることができる。
左辺から右辺への射を作るには、右辺をモナドにしてやって $F^*$ のuniversalityを使えばよい。
ここで積を定義するのに左項の分配法則 $(\mathrm{Id} + FF^*)^2 = (\mathrm{Id} + FF^*) + FF^*(\mathrm{Id} + FF^*)$ を使う。
合成 $\mathrm{Id} + FF^* \to F^* \to \mathrm{Id} + FF^*$ が $\mathrm{id}$ になることを示すのが少し面倒だが、$FF^*$ を $F$ で生成される右 $F^*$-加群だと思えれば簡単。
構成
上の同型をヒントにして、実際に $F^*$ を下から構築していくことができる（こともある）。
各順序数 $\alpha$ について、$F_\alpha$ を以下で再帰的に定義する。
$$F_\alpha \colon= \mathrm{Id} + FF_{<\alpha}, \qquad\text{where}\quad F_{<\alpha} \colon= \varinjlim_{\beta<\alpha} F_\beta$$
ここでinductive limitは自然に定義される射 $F_0\to F_1\to\dots\to F_\omega\to\dotsb$ についてとる。
この列が収束するとき、つまりある順序数 $\delta$ で $F_\delta\to F_{\delta+1}$ が同型となるならば、収束先 $F^*\colon=F_\delta$ が $F$ のFreeモナドになる。
$F^*$ の積は下から順に $F_\alpha F^*\to F^*$ を作ってlimitをとれば定義できるが、ここで左項について合成がlimitを保つこと $F_{<\alpha}F^* = \varinjlim_{\beta<\alpha}F_\beta F^*$ を使っている。
universalityの証明も、同様に与えられた $F\to M$ について一意的な $F_\alpha\to M$ を順に作っていけばよい。
例
- $F$ が任意個の和を保つとき、$F_0=\mathrm{Id}$, $F_1=\mathrm{Id}+F$, $F_2=\mathrm{Id}+F+F^2$,... と大きくなっていき、$F^* = F_\omega=\mathrm{Id}+F+F^2+\dotsb$ でストップする。
- $P\colon\mathcal{S}\mathit{et}\to\mathcal{S}\mathit{et}$ を冪集合をとる関手とする。すると $P_\alpha$ は際限なく大きくなって収束しない。実際もし $P^*$ があったとすれば、$P^*\varnothing$ が宇宙全体になってしまう。
- それに対し $P_{\mathrm{fin}}X$ を $X$ の有限部分集合全体とすると、$P_{\mathrm{fin}}\colon\mathcal{S}\mathit{et}\to\mathcal{S}\mathit{et}$ に対応する列は $\omega$ 世代で収束する。$P_{\mathrm{fin}}^*X$ は $X$ の元をアトムとする遺伝的有限集合全体になる。
この逆が成り立つか、つまりFreeモナドが存在するなら必ずそこに収束するか、というとそれは難しい気がする。大きい宇宙に目標があった場合小さい宇宙の順序数でいくらがんばっても届かなさそうだし……。ちゃんと考えないとよくわからない。
より一般に
このFreeモノイドの話は別に関手の圏に限らずもっと一般のモノイダル圏で話ができる。
ただし左項についてモノイダル積がlimitを保つこと $(\varinjlim_i X_i) \otimes Y = \varinjlim_i (X_i \otimes Y)$ が必要。
Haskellで
$F$ を f, $F^*$ を Free f とおきかえて $F^* = \mathrm{Id} + FF^*$ の関係をHaskellっぽく書くと、
data Free f a = A a | B (f (Free f a))
と書ける。A と B の記号に特に意味はないが、あえて同じ記号を濫用してわかりづらくすると
data Free f a = Pure a | Free (f (Free f a))
と巷でよく見るやつになる。データの構築も結局limitで下から作っていくのと似たようなことをしているはず。
ただ停止性やら遅延評価やら無限リストみたいなやつのことを考え出すとHaskellの圏は数学的にいろいろ汚くなるので（参考）あくまでメタファーくらいに思っておいたほうが精神的に平安が得られると思う。