class Applicative m => Monad m where
(>>=) :: forall a b. m a -> (a -> m b) -> m b
(>>) :: forall a b. m a -> m b -> m b
m >> k = m >>=\_ -> k
return :: a -> m a
return = pure
fail :: String -> m a
fail s = errorWithoutStackTrace s
それではデータ型\(Prod \ e \ a\)をコモナドのインスタンスとして定義しよう。これは次のようになる。
instance Functor (Prod e) where
fmap f (Prod e a) = Prod e (f a)
instance Comonad (Prod e) where
f =>= g =\(Prod e a) ->let b = f (Prod e a)
c = g (Prod e b)
in c
extract (Prod e a) = a
それではプログラムを使った例を示そう。図６：環境でカプセル化したデータ型\(P( e \ a)\)の実行例
プログラムのコードは次のようになっている。図７：環境でカプセル化したデータ型\(P( e \ a)\)のコード
\((=>=)\)の定義の中では二つの関数を入力にしている。即ち\(f : w \ a \rightarrow b\)と\(g: w \ b \rightarrow c\)である。\(g\)は入力として\(w \ b\)を必要とするので、\(f\)を利用して\(w \ b\)を出力するような関数\(extend\)を定義しよう。これは次のようになる。
instance Functor Stream where
fmap f Null = Null
fmap f (Cons a as) = Cons (f a) (fmap f as)
instance Comonad Stream where
extract (Cons a _) = a
duplicate Null = Null
duplicate (Cons a as) = (Cons (Cons a as) (duplicate as))
sumN :: Num a => Int -> (Stream a) -> a
sumN n Null =0
sumN n (Cons a as) =if n <=0then0else a + (sumN (n-1) as)
aveN :: Fractional a => Int -> Stream a -> a
aveN n Null =0
aveN n stm = (sumN n stm) / (fromIntegral n)
以下のプログラムで、\(zipstream\)はある時点での出力信号を求めるためのものである。これはストリームになっていて、この時点に入ってきた入力信号に対するこの時点の出力信号、その一つ前の時点で入ってきた入力信号に対するこの時点の出力信号、さらに一つ前の入力信号に対するこの時点の出力信号となっている。即ち、この時点までに入ってきた入力信号からの子の時点での出力信号の列である。\(zipstream\)は三つの入力を受ける。それらは \( f \ inp \ stm\)で、\(inp\)はインパルス応答、\(stm\)は入力信号である。なお、\(f\)はインパルス応答と入力信号のそれぞれに対する演算で、この場合は常に乗算である。
また、\(conv\)はある時点での出力信号の総和をとる。
zipstream :: Num a => (a -> a -> a) -> (Stream a) -> (Stream a) -> (Stream a)
zipstream f Null _ = Null
zipstream f _ Null = Null
zipstream f (Cons a as) (Cons b bs) = Cons (f a b) (zipstream f as bs)
conv :: Num a => (Stream a) -> a
conv Null =0
conv (Cons a as) = a + (conv as)
\(out\)は現時点までの出力信号の列である。
outC :: Num a => (Stream a) -> (Stream a) -> (Stream a)
outC inp stm = fmap conv (extend (zipstream (*) inp) stm)
--outC inp stm = fmap conv (fmap (zipstream (*) inp) (duplicate stm))
それではコモナドと随伴との関係を見てみよう。随伴には、内容は同じだが複数の定義がある。余単位(counit)・単位(unit)随伴はその中の一つで、それは次のようになっている。
圏\(\mathcal{C}\)と\(\mathcal{D}\)の余単位・単位随伴は二つの関手
\begin{eqnarray}
L: \mathcal{D} \rightarrow \mathcal{C} \\
R: \mathcal{C} \rightarrow \mathcal{D}
\end{eqnarray}
および二つの自然変換
\begin{eqnarray}
η: I_\mathcal{D} \rightarrow R \circ L \\
ε: L \circ R \rightarrow I_\mathcal{C}
\end{eqnarray}
であって(ηは単位、εは余単位と呼ばれる)、これらの合成
\begin{eqnarray}
L =L \circ I_\mathcal{D} \xrightarrow{L \circ η} L \circ R \circ L \xrightarrow{ε\circ L} L \\
R = I_\mathcal{D} \circ R \xrightarrow{η\circ R} R \circ L \circ R \xrightarrow{R \circ ε} R
\end{eqnarray}
がそれぞれ\(L\)と\(R\)上の恒等変換\(I_L,I_R\)となることである。これは三角恒等式(triangle identities)と呼ばれる。
図で表してみよう。随伴の定義に関する図は次のようになっている。図１７：随伴の定義にはいくつかあるが、単位(\(unit:I_\mathcal{D} \rightarrow R \circ L\))・余単位(\(counit:L \circ R \rightarrow I_\mathcal{C}\))を用いての定義も良く用いられる
また、三角恒等式を関図式で表すと次の通りだ。図１８：余単位・単位による随伴の定義の一部である三角恒等式の可換図式それではこの定義からコモナドを導くこととしよう。コモナドでの射\(δ,ε\)が、随伴を定めている\(η,ε\)から得られることを示せばよい。そこで、
\begin{eqnarray}
W=L \circ R
\end{eqnarray}
としてみよう。コモナド側の\(ε\)を得ることは簡単だ。
\begin{eqnarray}
ε : I_\mathcal{D} \xrightarrow{ε} L \circ R = W
\end{eqnarray}
それでは\(δ\)について考えよう。次のようにすればよい。
\begin{eqnarray}
δ : W = L \circ R = L \circ I_D \circ R \xrightarrow{L \circ η \circ R} L \circ R \circ L \circ R = W \circ W
\end{eqnarray}
class Applicative m => Monad m where
(>>=) :: forall a b. m a -> (a -> m b) -> m b
(>>) :: forall a b. m a -> m b -> m b
m >> k = m >>=\_ -> k
return :: a -> m a
return = pure
fail :: String -> m a
fail s = errorWithoutStackTrace s
\((>>=) :: forall \ a \ b. \ m \ a \rightarrow (a \rightarrow m \ b) \rightarrow m \ b\)
上の表で、式1は対応していることが分かる。しかし、式2、即ち\(join\)と\( (>>=)\)は対応しているとは即断しがたい。そこで、Haskellでの定義を変形してみよう。モナド\(m\)は関手なので、
\begin{eqnarray}
m \ a \rightarrow (a \rightarrow m \ b)
\end{eqnarray}
の部分は、下図のように表すことができる。図６：モナドの候補を確認する。Haskellの構造に変換し、Haskellで定義されているモナドの構造に対応しているかを観察する。そのためには、候補の\(join\)とHaskellの\(>>=\)が対応していることを示せばよい上図で、左側の射\(f: a \rightarrow m \ b\)を関手\(m\)によって、右側に移される。そして、\(m \ a \rightarrow (a \rightarrow m \ b)\)は、右側に移った射の始点\(m \ a\)が与えられた時、その終点をあたえる。このとき右側に移った射は\(fmap \ f \ (m \ a)\)である。これより、
\begin{eqnarray}
m \ a \rightarrow (a \rightarrow m \ b) & = & (fmap \ f \ (m \ a)) \\
& = & m (f (a)) \\
& = & m (m \ b)
\end{eqnarray}
となる。まとめると、
\begin{eqnarray}
m \ a \rightarrow (a \rightarrow m \ b) \rightarrow m \ b \\
= m (m \ b) \rightarrow m \ b
\end{eqnarray}
である。\(b\)を\(a\)で置き換えると、
\begin{eqnarray}
m (m \ a) \rightarrow m \ a
\end{eqnarray}
となり、\(join\)同じであることが分かる。
\begin{eqnarray}
η &:& A & \rightarrow & T(A) \\
μ &:& T(T(A) & \rightarrow & T(A)
\end{eqnarray}
さらに、\(T(A),T(T(A)),…\)は同じ薄茶色で表し、薄緑色の部分をなくすと、前に示した図は次のように表すことができる。図７：一般的なモナドの定義に近づけるために、\( return,join\)を\(η,μ\)で置き換える上の式をもう少し変形してみよう。恒等射\(I:A \rightarrow A\)を用いると上記の式は次のようになる。
\begin{eqnarray}
η &:& I(A) & \rightarrow & T(A) \\
μ &:& T(T(A) & \rightarrow & T(A)
\end{eqnarray}
上記の式は任意の\(A\)について成り立つので、\(A\)を省くと
\begin{eqnarray}
η &:& I & \rightarrow & T \\
μ &:& T \circ T & \rightarrow & T
\end{eqnarray}
と記述することができる。そこで、圏\(\mathcal{C}\)を対象とし、関手\(T\)を射とし、モナドを表す圏\(\mathcal{D}\)をつぎのように定義できる。
圏\(\mathcal{D}\)の構成
対象：圏\(\mathcal{C}\)
射：\(T: \mathcal{C} \rightarrow \mathcal{C} \)
恒等射：\(I_\mathcal{C} \)
合成：\(\circ\)
そして、次のように、単位律、結合律を満たすものとする。
単位律：\(I_\mathcal{C} \circ T= I_\mathcal{C} = T \circ I_\mathcal{C} \)
結合律：\( (T \circ T) \circ T = T \circ (T \circ T) \)
圏\(\mathcal{D}\)は、さらに
\begin{eqnarray}
η&:& I_\mathcal{C} & \rightarrow & T \\
μ&:& T \circ T & \rightarrow & T
\end{eqnarray}
を満たすものとする。ここでは、\(η: I \rightarrow T \)から\(η: I_\mathcal{C} \rightarrow T \)に変えている。恒等射の定義域が単純な実体の領域から表層の領域まで含むようになったが、\(η: I_T \rightarrow T \circ T \rightarrow T \)であることから、矛盾なく拡張することが可能である。
圏\(\mathcal{C}\)と\(\mathcal{D}\)の余単位・単位随伴は二つの関手
\begin{eqnarray}
L: \mathcal{D} \rightarrow \mathcal{C} \\
R: \mathcal{C} \rightarrow \mathcal{D}
\end{eqnarray}
および二つの自然変換
\begin{eqnarray}
η: I_\mathcal{D} \rightarrow R \circ L \\
ε: L \circ R \rightarrow I_\mathcal{C}
\end{eqnarray}
であって(ηは単位、εは余単位と呼ばれる)、これらの合成
\begin{eqnarray}
L =L \circ I_\mathcal{D} \xrightarrow{L \circ η} L \circ R \circ L \xrightarrow{ε\circ L} L \\
R = I_\mathcal{D} \circ R \xrightarrow{η\circ R} R \circ L \circ R \xrightarrow{R \circ ε} R
\end{eqnarray}
がそれぞれ\(L\)と\(R\)上の恒等変換\(I_L,I_R\)となることをいうとなっている。これは三角恒等式(triangle identities)と呼ばれる。これを可換図式で示そう。図１４：余単位・単位による随伴の定義の一部である三角恒等式の可換図式それではこの定義からモナドを導くこととしよう。圏\( \mathbf{End}_\mathcal{C} \)での射\(η,μ\)が、随伴を定めている\(η,ε\)から得られることを示せばよい。そこで、
\begin{eqnarray}
T=R \circ L
\end{eqnarray}
としてみよう。モナド側の\(η\)を得ることは次に示すように簡単である。
\begin{eqnarray}
I_\mathcal{D} \xrightarrow{η} R \circ L = T
\end{eqnarray}
それでは\(μ\)について考えよう。次のように変換して求めることができる。
\begin{eqnarray}
T \circ T = R \circ L \circ R \circ L \xrightarrow{R \circ ε \circ L} R \circ I_\mathcal{C} \circ L = R \circ L = T
\end{eqnarray}
圏\( \mathbf{End}_\mathcal{C} \)の単位律、結合律を随伴から得てみよう。まず単位律から始める。
\begin{eqnarray}
L \xrightarrow{L \circ η} L \circ R \circ L \xrightarrow{ε\circ L} L \\
R \xrightarrow{η\circ R} R \circ L \circ R \xrightarrow{R \circ ε} R
\end{eqnarray}
と、およびそれぞれで左辺と右辺は恒等変換になっていることを利用すると
\begin{eqnarray}
T \circ I_\mathcal{D} = R \circ L \circ I_\mathcal{D} \xrightarrow{R \circ L \circ η} R \circ L \circ R \circ L \xrightarrow{R \circ ε \circ L} R \circ L = T \\
I_\mathcal{D} \circ T = I_\mathcal{D} \circ R \circ L \xrightarrow{η \circ R \circ L} R \circ L \circ R \circ L \xrightarrow{R \circ ε \circ L} R \circ L = T
\end{eqnarray}
を得る。またそれぞれで左辺と右辺は恒等変換になっていることもわかる。可換図式で示すと下図のようになる。図１６：随伴の定義からモナドの単位律を得る
*Main Control.Monad> f x rest =\b ->if b then rest >>= return . (x:) else rest
*Main Control.Monad> [True, False] >>= f 1 [[2,3],[2],[3]]
[[1,2,3],[1,2],[1,3],[2,3],[2],[3]]
少し、工夫をして、\(x\)の値を外から与えられるようにしよう。
\x -> const [True, False] x >>=\b ->if b then rest >>= (return . (x:)) else rest
確認しよう。
*Main Control.Monad> g rest =\x -> const [True, False] x >>=\b ->if b then rest >>= (return . (x:)) else rest
*Main Control.Monad> g [[2,3],[2],[3]] 1
[[1,2,3],[1,2],[1,3],[2,3],[2],[3]]
56号線を北上していくと左側に目的地のGarden Island Chocolateが出てくる。しかし、Googleの道案内によれば、ここを通り越して、はるか先のハナレイ国立野生棒物保護区のロータリーで引き返すようになっている。56号線は高速道路なので、Googleは左折することができないと認識している。このため、Uターンできる地点を探しているのだ。我々はこの道案内に従ったために損をした。危うく集合時間に間に合わないところだった。
