Free モナドについて考えたこと メモ
なんかはてなブログ重くないですか？タスクマネージャを開いて確かめたので間違いない
Free モナド
こういうやつです 1 (ただし、fはFunctorのインスタンスであるとする)
data Free f a = Pure a | Join (f (Free f a))
JoinじゃなくてFreeと書かれていることもあるけど、今回はJoinで行きます
これを GADTs で書くと、以下のようになる:
data Free f a where Pure :: a -> Free f a Join :: f (Free f a) -> Free f a
なんてこった！これではまるでMonadのreturn(Applicativeのpure)やjoinにそっくりではないか！ということで、なんとなくモナドっぽいデータ構造になっていることがわかる
実際、以下のようにしてMonadのインスタンスになるらしい
instance (Functor f) => Monad (Free f) where return = Pure Pure a >>= f = f a Join x >>= f = Join $ fmap (>>= f) x
だけど、本当か？「モナドっぽい見た目だからモナドです」なんて小学生の屁理屈の亜種みたいなものが、本当にモナド則を満たすのか？というお気持ちが発生してしまう
モナド則
return x >>= f == f x -- (1) m >>= return == m -- (2) (m >>= f) >>= g == m >>= (\n -> f n >>= g) -- (3)
確かめてみましょう！
return x >>= f == Pure x >>= f -- `return`の定義 == f x -- `(>>=)`の定義
Pure a >>= return == return a -- `(>>=)`の定義 == Pure a -- `return`の定義 Join x >>= return == Join $ fmap (>>= return) x -- `(>>=)`の定義 == Join $ fmap id x -- 帰納的に (2) が成り立つ (*) == Join x -- ファンクタ則
(Pure a >>= f) >>= g == f a >>= g -- `(>>=)`の定義 == (\n -> f n >>= g) a -- ベータ変換 == Pure a >>= (\n -> f n >>= g) -- `(>>=)` の定義 (Join x >>= f) >>= g == (Join $ fmap (>>= f) x) >>= g -- `(>>=)` の定義 == Join $ fmap (>>= g) (fmap (>>= f) x) -- `(>>=)` の定義 == Join $ fmap (>>= g) . fmap (>>= f) $ x -- 関数合成 == Join $ fmap ((>>= g) . (>>= f)) x -- ファンクタ則 == Join $ fmap (\a -> (a >>= f) >>= g) x -- 関数合成の展開 == Join $ fmap (\a -> a >>= (\n -> f n >>= g)) x -- 帰納的に (3) が成り立つ (*) == Join $ fmap (>>= (\n -> f n >>= g)) x -- セクション == Join x >>= (\n -> f n >>= g) -- `(>>=)`の定義
(*) ここは私が厳密性に確信を持てていない (多分大丈夫だけど) (わかる人は教えてください)
というわけで、(一部怪しい所もありましたが) 無事モナド則を証明できました！今日から胸を張ってFreeを使うことができますね
......っておいおい、これじゃただモナド則を証明しただけになっちゃうよ〜〜〜！！！トホホ〜〜 (終) (もしかしたらあとで何か書くかも)
