to2yの日記

■ 11.1 モナドとは何か

もともと数学の圏論の分野で使用される概念

代表的なモナド

+ IOモナド（アクション）

+ Maybe

+ List

Haskellでは、Monadという型クラスのインスタンス

Monadクラス

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

>>=はbindと読む。

#(>>=)は a -> (a -> b) -> bをモナド適用後も保証しているイメージか

モナド則

モナドとなるためには、>>=,returnがモナド則を満たす必要がある。

1. (return x) >>= f == f x
2. m >>= return == m
3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)

モナドに関する参考文献

All About Monads

最初の規則は return が >>= に関して左単位元になっていることを要請しています。二番目の規則は return が >>= に関して右単位元になっていることを要請しています。そして、三番目の規則は >>= に関する一種の結合法則です。三番目の規則に従えば、モナドをつかった do 記法のセマンティクスは一貫性をもちます。

http://haskell.cs.yale.edu/haskellwiki/Books#Using_monads:モナドに関する文献index]

CiteSeerX (PDF)

3.Monad Lawsにて、Monad則を用いて、Addが結合性を満たすことを証明している。

雑感

Monadの典型は、例外、入出力、状態の３つ？

■ 11.2 Maybeモナド

data Maybe = Nothing | Just a drving (Eq,Ord)

lookup :: (Eq a) => a -> [(a,b)] -> Maybe b 

lookup関数は、連想リスト(alist)とキーから対応するペアの値が存在する場合に(Just a)をそうでない場合には、Nothingを返す。

Maybeモナドの目的（利点）

「関数を連続して適用する場合に、どこかでNothingになったら、その時点であとの処理をとりやめる」処理をスマートに記述できる。

#通常は大域脱出として実現するのが普通か

Maybeモナドの仕組み

instance Monad Maybe where
  (Just x) >>= f = f x
  Nothing >>= f  = Nothing
  return x       = Just x

モナド則を満たしていることの証明

モナド則1

  (return x) >>= f
== (Just x) >>= f 
== f x

モナド則2

   m >>= return
(1)mがJust xの場合
    (Just x) >>= return
==  return x
==  Just x == m
(2)mがNothingの場合
    Nothing >>= return
==  Nothing == m

モナド則3

(1) mがJust xの場合
   左辺
== (Just x >>= f) >>= g
== (f x) >>= g
   右辺
== (Just x) >>= (\x -> f x >>= g)
== (\x -> f x >>= g) x
== (f x) >>= g
(2)mがNothingの場合
   左辺
== (Nothing >>= f) >>= g
== (Nothing) >>= g
== Nothing
   右辺
== Nothing >>= (\x -> f x >>= g)
== Nothing

#>>=の左辺が(f x)の形式になっているのがあやしいですが

■ 次回はこの続き

9/10 21:00～