読者です 読者をやめる 読者になる 読者になる

bitterharvest’s diary

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

HaskellドリルⅤ モナドの理論的な背景

1.モナド

圏論の入門書の最後のほうに出現するのがモナドである。そこでは、随伴性という概念を用いてモナドは定義されている。このため、モナドを本当に理解しようとしたら、圏論の基礎的な知識を持たなければならないのだが、ここでは、随伴性という専門用語を用いずに、モナドを説明する。

関手(ファンクタ)を用いるとモナドは次のように定義できる。

モナドは関手\(\mathcal{M}:\mathcal{C} \rightarrow \mathcal{C}\)で、\(\mathcal{C}\)内のすべての対象\(X\)に対して、次の二つの射を有する。
1)\(unit_{X}:X \rightarrow \mathcal{M} (X)\)
2)\(join_{X}:\mathcal{M}(\mathcal{M}(X)) \rightarrow \mathcal{M} (X)\)

モナドが関手であることから、下図の性質を継承する。
f:id:bitterharvest:20150110053001p:plain
但し、上の図で、モナドは自身の圏への写像であることを忘れてはならない。

また、モナドは二つの特別な射を有している。これらの関数を説明する前にモナドとはどのようなものかを直感的に理解しておくことが必要である。数学的には正確ではないが、たとえ話で説明する。数式を表す時は、計算の順序を示したり、あるいは、読みやすくするために、カッコを用いる。しかし、カッコを余分につけすぎるとカッコを減らしたいという要求も生まれる。カッコをつけることがモナドを施すことに相当し、カッコを外すことが施されたモナドを解くことに相当する。「カッコをつけること」を「意味を持たせる」と理解し、「カッコを外すこと」を「忘れる」と理解すると、モナドの数学的な概念に近づいてくるが、ここでは、モナドとはカッコをつけたり外したりすることを抽象的に行っていると理解しておく。

そこで、先ほどのモナドの二つの特別な関数だが、\(unit\)はモナドを施す(カッコをつける)ことに相当し、\(join\)はモナドを解く(カッコをはずす)ことに相当する。

2.定義が異なる

Haskellにおいてもモナドは重要な役割を果たすが、圏論でのそれとは、定義が異なっている。Haskellでは上記の定義を次のように表している。

Class Functor m => Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b

上記の記述で、returnが\(unit\)に、(>>=)が\(join\)に対応するのだが、これらが同じ事を表しているという説明は後ですることにして、Haskellでのモナドについてもう少し説明する。

上記の定義から次の法則を導くことができる。

  return a >>= f    = f a
  m a >>= return    = m a
  (m a >>= f) >>= g = m a >>= (\x -> f x >>= g)

return a >>= f は、return a の結果(aにモナドを施すことでm aとなったもの)にfを利用して、>>=を施すものである。その結果はf aである。ここで、fの型シグネチャは次のようになっている。

  f :: Monad m => a -> mb

従って、fはモナドになる前の純粋なaをモナドになったm bへと変換する。return a >>= f はm a >>= fと同じなので、外側から見ている限りは、モナドのm a がモナドのm bに変換されたようにしか見えない。しかし、fはモナドのm aからの変換を行っているわけではない。fはモナドになっていない純粋なaからの変換である。Haskellでのモナドを理解するとき、fのこの性質を忘れてはいけない。これは、(>>=)によってモナドを一つ解くことを意味する。これは\(join\)の性質でもあった。

m a >>= returnは、m aからモナドを解いたaに、returnによってモナドを施すので、出力はm aとなる。

(m a >>= f) >>= g = m a >>= (\x -> f x >>= g)も同じように考えることができる。

3.圏論でのモナドHaskellでのモナドは等価である

(>>=)がモナドを解くと理解したとしても、\(join\)には似ているように思えない(>>=)が、haskellでは\(join\)の代わりに用いている。これは、二つの定義が同じであることに起因していて、それぞれの分野で都合のよいほうを用いるためだが、ここでは、両者の定義が等価であることを観察する。

Monadの定義は一つではなく、等価なものがいくつか存在する。その中で、\(join\)を用いて定義する方法がある(ここでの議論はMonads in Haskell: Algebraに詳しい説明がある)。

class (Functor m) => Monad' m where
  join :: m (m a) -> m a
  return' :: a -> m a
  (>>~) :: m a -> (a -> m b) -> m b
  x >>~ f = join (fmap f x)

ここでのモナドの定義は上の二つjoinとreturn'だけである。(>>=)に変わる(>>~)はjoinを用いて定義した。
下図にreturn, >>=, joinの関係を示す。
f:id:bitterharvest:20150113220852p:plain

4.Maybeを用いて検証する

MaybeはPreludeでは、ファンクタとして、また、モナドとしても定義されている。従って、モナドでの関数を使ってその動きを観察すると次のようになる。

class (Functor m) => Monad' m where
Prelude> return 3 :: Maybe Integer
Just 3
Prelude> Just 3 >>= (\x -> Just (x + 1))
Just 4
Prelude> Nothing >>= (\x -> Just (x + 1))
Nothing

そこで、MaybeをMonad'のインスタンスとし、同様に働くか観察する。
インスタンス化は次のように行う。

instance Monad' Maybe where
  join (Just (Just x)) = Just x
  join (Just Nothing) = Nothing
  return' a = Just a

これを利用して、return'と(>>~)の動きを調べる。

*Main> return' 3 :: Maybe Integer
Just 3
*Main> Just 3 >>~ \x -> return (x + 1)
Just 4
*Main> Nothing >>~ \x -> return' (x + 1)
Nothing

同じような結果が得られることが分かる。

5.Haskellの定義から圏論の定義を導き出す。

returnとjoinを用いてモナドを定義すると、これから、>>=が導き出せることが分かったので、逆も同じであると考えることができる。そこで、returnと>>=を定義して、joinが導き出せることを示す。例によって、次のように定義する。(>>#)は、関数の衝突をつけるために別名にしたが、(>>=)と同じである。ここでのモナドは(>>#)とreturn"で定義し、joinはこれら二つの定義を使って定めた。

class (Functor m) => Monad" m where
  (>>#) :: m a -> (a -> m b) -> m b
  return" :: a -> m a
  join" :: m (m a) -> m a
  join'' x = x >># id

Maybeをこのクラスのインスタンスにすると次のようになる。

instance Monad'' Maybe where
  Nothing >># f = Nothing
  Just x >># f = f x
  return'' a = Just a

ここでも同じように、Maybeを利用してみると次のようになる。

*Main> return'' 3 :: Maybe Integer
Just 3
*Main> Just 3 >># \x -> return (x + 1)
Just 4
*Main> Nothing >># \x -> return' (x + 1)
Nothing

正しく動いているので、次にjoin''の動きを観察する。

*Main> Join'' (Just (Just 3))
Just 3
*Main> Join'' (Just Nothing)
Nothing
*Main> Join'' Nothing
Nothing

これも正しく動いていることが分かる。

joinについては次の法則が成り立つ。

return . f = fmap f . return
join . return        = id
join . fmap return   = id
join . fmap join     = join . join
join . fmap (fmap f) = fmap f . join

これで、(完璧には証明していないが)圏論でのモナドHaskellでのモナドとが同じであることがほぼ理解できた。

6.モナドの例

圏論からのモナドの例を挙げる。ここでは冪集合を考える。冪集合は、ある集合が与えられた時に、その要素からなる部分集合の全てを要素とする集合である。例えば、集合\(S=\{x,y,z\}\)の冪集合\(P(S)\)は\(\{\{\},\{x\},\{y\},\{z\},\{x,y\},\{x,z\},\{y,z\},\{x,y,z\}\}\)である。

さらに、冪集合\(P(S)\)は集合なので、この冪集合も考えることができる。これは
\begin{eqnarray}
P(P(S))& = & \{\{\},\{x\},\{y\},\{z\},\{x,y\},\{x,z\},\{y,z\},\{x,y,z\},\{\{\},\{x\}\},\{\{\},\{y\}\}, \\
& & ...,\{\{\},\{x,y,z\}\},\{\{x\},\{y\}\},\{\{x\},\{z\}\},...\}
\end{eqnarray}
となる。これも集合なので、さらにこの集合の冪集合を考えることができる。

そこで、冪集合の関数\(P\)を集合から集合への関手(ファンクタ)とする。この時、
1)\(unit_S(x) = \{x\}\)、ここで、\(x \subset S\)かつ\(\{x\} \in P(S)\)。即ち、\(x\)は\(S\)の部分集合であるとき、\(\{x\}\)は\(P(S)\)である。
2)\(join_S(L) = \cup{L}\)、ここで、\(L \in P(P(S))\)(\(L\)は\(S\)の一つあるいは複数の部分集合の集合で、\(\cup{L}\)はこれら部分集合の和集合である。例えば、\(L=\{\{\},\{\{\},\{x,y\}\},\{\{x\},\{x,y\}\}\}\)であれば、\(join_S(L) = \{x,y\}\)である)。従って、\(\cup{L} \in P(S)\)である。

上記の\(unit\)と\(join\)がモナドの条件を満たしていることから冪集合の関数\(P\)はモナドである。

7.クラス階層

ファンクタとモナドに関連するクラス階層は図のようになっている。ファンクタとモナドの間にはアプリカティブという型クラスが存在する。アプリカティブは、現在のPleludeには含まれていないが、7.10より含まれる予定である。
f:id:bitterharvest:20150114095349p:plain

8.問題

それでは問題を解いてみる。

問題1:次の出力を求めなさい。
1)fmap (++"?") (Just "Are you sure")
2)fmap (++"?") Nothing
3)Just 5 >>= \x -> return (x * x)
4)Nothing >>= \x -> return (x * x)
5)return "Yes or No" :: Maybe String

問題2:x >>~ f = join (fmap f x)がx >>= fと等価であることを証明しなさい。

問題3:join'' x = x >># idが\(join x\)と等価であることを証明しなさい。

問題4:次の法則が成り立つことを証明しなさい。
1)return a >>= f = f a
2)m a >>= return = m a
3)(m a >>= f) >>= g = m a >>= (\x -> f x >>= g)

問題5:次の法則が成り立つことを証明しなさい。
1)return . f = fmap f . return
2)join . return = id
3)join . fmap return = id
4)join . fmap join = join . join
5)join . fmap (fmap f) = fmap f . join

問題6:Maybeをファンクタのインスタンスとして定義しなさい。

問題7:左右のどちらかを選ぶ関数Eitherはファンクタであるとともに、モナドである。Eitherをファンクタのインスタンスとして定義した後、モナドインスタンスとして定義しなさい。

問題8:リストを作成する関数[ ]もファンクタであるとともに、モナドである。[ ]をファンクタのインスタンスとして定義した後、モナドインスタンスとして定義しなさい。

問題9:冪集合にする関数PをファンクタのインスタンスとしてHaskellで定義しなさい。

問題10:冪集合にする関数PをモナドインスタンスとしてHaskellで定義しなさい。