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\),として表すことにしよう。
下図の可換図式に示すように、\(return\)では、\(a\)は恒等関手\(Id\)となり、\(m \ a \)は関手\(T\)となる。
これより、となる。は、\(\mathcal {C}\)の内部構造を維持しての関手から関手への写像となっているので、自然変換である。
また、\(T \circ T\)を\(T^2\)と書くと、下図の可換図式より\(\mu:: T^2 \rightarrow T \)を得る。これも内部構造を保っての関手から関手への写像なので、自然変換である。
ところで、モナドが圏となるためには、\(T\)に対して結合律が成り立つ必要がある。即ち、\(T \circ T^2= T^2 \circ T\)でなければならない。それでは、左式を\(\mu\)を用いて表してみよう。
\(T \circ T^2\)を可換図式で表すと次のようになる。なお、下図で\(T\)から\(T\)への恒等な自然変換を\(I_T\)で表した。
この可換図式より、\(\mu \circ I_T=\mu \)を得る。
\(T^2 \circ T\)を可換図式で表すと次のようになる。
この可換図式より、\( I_T \circ \mu =\mu \)を得る。
これより\(\mu \circ I_T=\mu = I_T \circ \mu \)が満たさなければならないことが分かる。
これを可換図式で表現すると次のようになる。
モナドが圏であるためには、関手\(T\)は単位律をも満たす必要がある。単位律は\(T \circ Id = T = Id \circ T\)である。
\(T \circ Id \)より下図の可換図式を得る。
これよりを得る。
\(Id \circ T \)より下図の可換図式を得る。
これよりを得る。
従って、が満たさなければならないことが分かる。
これを可換図式で表現すると次のようになる。
\(I_T\)は\(T\)と見なしてもよいので、Mac LaneやAwodeyの教科書には次の可換図式が掲載されている。
モナドの圏としての構成:
1) 対象:関手\(T\)、恒等関手\(Id\)
2)射:\(\mu\),
3)ドメイン、コドメイン:\(\mu: T^2 \rightarrow T\),
4)恒等射:\(I_T: T \rightarrow T\)
5)合成:\(\mu\)とを合成したものは、下図に示すように、組合せによらず\(\mu\)となる。
さらに、次の二つを満たす必要がある。
\( \mu \circ T = T \circ \mu \)