bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

モナドと自然変換

12.圏論でのモナド

Haskellでのモナドについて論じてきたが、モナド圏論の中の一つの圏でもある。そこで、ここではモナドが圏となるための条件を求めて見よう。

圏論においては自然変換は重要な役割をなすが、モナドは自然変換が主要な枠組みとなっている数学概念でもある。

まず、Haskellではモナドは\(join\)と\(return\)を用いて次のように定義した。

class Functor m => Monad m where
  join :: m (m a) -> m a
  return :: a -> m a

また、Haskellでの記述を圏論での記述に直すことを考えよう。モナドは自身の圏に写像する関手である。そこで、モナドの圏\(\mathcal {C}\)は、対象が関手で、射が関手間の写像(自然変換)として構成することにしよう。そして、Haskellモナド\(m\)は圏論での関手\(T\)として、\(join,return\)は圏論での自然変換\(\mu\), \eta として表すことにしよう。

下図の可換図式に示すように、\(return\)では、\(a\)は恒等関手\(Id\)となり、\(m \ a \)は関手\(T\)となる。
f:id:bitterharvest:20170905115110p:plain
これより、\eta :: Id \rightarrow Tとなる。 \etaは、\(\mathcal {C}\)の内部構造を維持しての関手から関手への写像となっているので、自然変換である。

また、\(T \circ T\)を\(T^2\)と書くと、下図の可換図式より\(\mu:: T^2 \rightarrow T \)を得る。これも内部構造を保っての関手から関手への写像なので、自然変換である。
f:id:bitterharvest:20170905115136p:plain
ところで、モナドが圏となるためには、\(T\)に対して結合律が成り立つ必要がある。即ち、\(T \circ T^2= T^2 \circ T\)でなければならない。それでは、左式を\(\mu\)を用いて表してみよう。

\(T \circ T^2\)を可換図式で表すと次のようになる。なお、下図で\(T\)から\(T\)への恒等な自然変換を\(I_T\)で表した。
f:id:bitterharvest:20170905115156p:plain
この可換図式より、\(\mu \circ I_T=\mu \)を得る。

\(T^2 \circ T\)を可換図式で表すと次のようになる。
f:id:bitterharvest:20170905115213p:plain

この可換図式より、\( I_T \circ \mu =\mu \)を得る。
これより\(\mu \circ I_T=\mu = I_T \circ \mu \)が満たさなければならないことが分かる。

これを可換図式で表現すると次のようになる。
f:id:bitterharvest:20170905115233p:plain

モナドが圏であるためには、関手\(T\)は単位律をも満たす必要がある。単位律は\(T \circ Id = T = Id \circ T\)である。

\(T \circ Id \)より下図の可換図式を得る。
f:id:bitterharvest:20170905115248p:plain
これより I_T \circ \eta = \etaを得る。

\(Id \circ T \)より下図の可換図式を得る。
f:id:bitterharvest:20170905115312p:plain
これより \eta \circ I_T = \etaを得る。

従って、 I_T \circ \eta =\eta = \eta \circ I_T が満たさなければならないことが分かる。

これを可換図式で表現すると次のようになる。
f:id:bitterharvest:20170905115331p:plain

\(I_T\)は\(T\)と見なしてもよいので、Mac LaneやAwodeyの教科書には次の可換図式が掲載されている。
f:id:bitterharvest:20170905115350p:plain


最後に圏論としてのモナドをまとめよう。

モナドの圏としての構成:
1) 対象:関手\(T\)、恒等関手\(Id\)
2)射:\(\mu\), \eta
3)ドメイン、コドメイン:\(\mu: T^2 \rightarrow T\), \eta:: Id \rightarrow T
4)恒等射:\(I_T: T \rightarrow T\)
5)合成:\(\mu\)と \etaを合成したものは、下図に示すように、組合せによらず\(\mu\)となる。
f:id:bitterharvest:20170905115410p:plain

さらに、次の二つを満たす必要がある。
\( \mu \circ T = T \circ \mu \)
 T \circ \eta =\eta = \eta \circ T

以上で、圏論におけるモナドの構造を示すことができた。