MonoidもMonadもモノイドだって話 - Pixel Pedals of Tomakomai

わかめのモナド浸しと第6回スタートHaskell2で「モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？」という話をしてきた。スライドは以下。

.tar.gz の方はHaskellでの説明だったので、検証用コードも書いてみてgistに上げてる。QuickCheckとか使わずに値一個与えてみてるだけだけど、型が通ることくらいは確認できるかと。以下、検証用コードについて解説する。

MonoidはHaskの圏のモノイド

まず、Monoidの方。図式はスライドを見てもらうとして、ソースは以下。満たすべきは各図式の時計回りと半時計回りが等しいことであり、具体的には、モノイドであれば clockwiseX == anticlockwiseX である必要があるという意味である。

assoc :: ((a, b), c) -> (a, (b, c))
assoc ((x, y), z) = (x, (y, z))

prod :: (a -> b, c -> d) -> (a, c) -> (b, d)
prod (f, g) (x, y) = (f x, g y)

mappend' :: Monoid a => (a, a) -> a
mappend' = uncurry mappend

mempty' :: Monoid b => a -> b
mempty' = const mempty

ここまでは下準備。assocはモノイダル圏の定義のαだが、要は型合わせ。あと、図式に直積を使いたかったので、関数の直積をとるprodやらuncurry化したmappend'を用意する。memptyは射じゃないと困るので、constする。

clockwise1 :: Monoid a => ((a, a), a) -> a
clockwise1 = mappend' . prod (id, mappend') . assoc

anticlockwise1 :: Monoid a => ((a, a), a) -> a
anticlockwise1 = mappend' . prod (mappend', id)

こちらは最初の四角形の図式。clockwise (x, y, z)を計算するとx `mappend` (y `mappend`) z、antiの方は(x `mappend` y) `mappend` zとなり、Monoid則の3つ目となる。

clockwise2 :: Monoid a => ((), a) -> a
clockwise2 = mappend' . prod (mempty', id)

anticlockwise2 :: Monoid a => ((), a) -> a
anticlockwise2 = snd

clockwise3 :: Monoid a => (a, ()) -> a
clockwise3 = fst

anticlockwise3 :: Monoid a => (a, ()) -> a
anticlockwise3 = mappend' . prod (id, mempty')

こちらは次の三角形2つの図式で、clockwise2が左側、clockwise3が右側の三角形を示す。clockwise2 ((), x)はmempty `mappend` x、antiの方はxとなるのでMonoid則の1つ目となる。clockwise3も同様で、これがMonoid則の2つ目。

これで四角と三角の図式がMonoid則を表すことがわかった。

MonadはHaskの自己関手の圏のモノイド

Haskの自己関手の圏は、対象がFunctor fであり、2つのFunctor fとgの間の自然変換を射とするものである。自然変換とは具体的には s :: f a -> g a のようなもの。スライドの図式は、型aに対するコンポーネントで書いてある。この図式がモナド則を表現していることを示すのだけど、通常の3つの規則だと説明に合わないので、同値であることが証明されている以下の規則を用いる。

join . fmap join = join . join
join . fmap return = join . return = id

見ての通りポイントフリーの式となっている。なので、Monoidのときは型aからxという値を取り出してポイントワイズな等式を作ったが、ここではポイントフリーな等式を作っていく。

早速gistのコードを見ていこう。

natComp :: (Functor m1, Functor m2, Functor m3, Functor m4) =>
           (forall a.m1 a -> m2 a) -> (forall a.m3 a -> m4 a)
                                           -> (forall a.m3 (m1 a) -> m4 (m2 a))
s `natComp` t = (fmap s) . t

まず、自己関手の圏にモノイダル圏の構造を入れるために、射の間の演算を準備している。具体的に言えば、これは自然変換sとtの水平合成にあたる。定義はwikipediaとか参照。自然変換を扱う関係でRankNTypes拡張が必要になる。

join' :: Monad m => Compose m m a -> m a
join' (Compose m) = join m

return' :: Monad m => Identity a -> m a
return' (Identity x) = return x

この2つも下準備。joinは本来m mからmへの自然変換だが、Haskellではm mはFunctor型ではないので、そのままでは自然変換の定義に合わない。そこで、Data.Functor.Compose を使って合成した関手 Compose m m を使う必要がある。join' はそこを踏まえて型を合わせたもの。

return' も同様の理由で a -> m a だと恒等関手が隠れてしまっているので、Identityを明示するように型を合わせている。

clockwise1 :: (Functor m, Monad m) => m (m (m a)) -> m a
clockwise1 = join . (join' `natComp` id) . iso
    where iso :: Functor f => f (f (f a)) -> f (Compose f f a)
          iso = fmap Compose

anticlockwise1 :: (Functor m, Monad m) => m (m (m a)) -> m a
anticlockwise1 = join . (id `natComp` join') . iso
    where iso :: Functor f => f (f a) -> Compose f f a
          iso = Compose

道具が揃ったのでまず1つ目の四角形の図式から。clockwise1の右に向かう矢印は、スライドでは簡単のために単にfmap joinと書いたが、この圏での演算は自然変換の水平合成だったので、厳密にはnatCompを使う必要がある。Monoidでprod (id, mappend')だったものが、MonadではnatComp join' idになっており、比較すると同じ図式から式を起こしていることがなんとなくわかるだろう。

isoは同型を表す関数で、気分としてはidみたいなものだと思ってよい。f (f (f a))もf (Compose f f a)も表現したいのは(f f f) aなので、同じだよねという意味を込めている。実際型を合わせているだけで何もしていない。

ここでclockwise1はjoin . fmap joinとなり、anticlockwise1はjoin . joinとなるので、今回使っているモナド則2つのうちの1つめを表すことがわかる。

(余談だが、ここでjoin'ではなくてjoinが登場しているが、これはnatCompにて戻り値にComposeを使わなかったため。ここもComposeを使った方が一貫性は出る気がする。)

clockwise2 :: (Functor m, Monad m) => m a -> m a
clockwise2 = join . (id `natComp` return') . iso
    where iso :: b -> Identity b
          iso = Identity

anticlockwise2 :: (Functor m, Monad m) => m a -> m a
anticlockwise2 = id

clockwise3 :: (Functor m, Monad m) => m a -> m a
clockwise3 = id

anticlockwise3 :: (Functor m, Monad m) => m a -> m a
anticlockwise3 = join . (return' `natComp` id) . iso
    where iso :: Functor f => f b -> f (Identity b)
          iso = fmap Identity

こちらは三角の図式で、clockwise2が左の三角形、clockwise3が右の三角形を表したもの。ここのisoもIdentityを付けたり外したりという型合わせのためにある。clockwise2はjoin . returnなので、今回使っているモナド則の2つめの規則の真ん中の項と3番目の項(id)の等式を表す。anticlockwise3の方はjoin . fmap returnなので、これでモナド則の2つめの式を表していることがわかった。