モナド則再び

モナド則が未だに分りません。しかし、ちょっとだけ理解が進んだのでメモしておきます。

復習

まず、「モナドのすべて」から、モナド則を引用します。

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

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

bind で考えていると、よく理解できないので、「The Haskell School of Expression」を参考に、do に書き変えてみます。

The Haskell School of Expression: Learning Functional Programming through Multimedia

規則1

規則1は、こういう意味です。

do y <- return x
   f y

== f x

しかし何の役に立つのか分りません。まず前者を書いて、後者に書き変えるという場面に出会ったことがないからです。

規則2

規則2は、こう書き換えられます。

do x <- m
   return x

== m

これは役に立ちますね。

たとえば、こういう風に略記できるからです。

do x <- m
   y <- f x
   z <- g y
   return z

==

do x <- m
   y <- f x
   g y

規則3

こういうことらしいです。

-- 規則3の左側
do x <- m
   y <- f x
   g y

==
-- 定義にある置き換え規則から、左側の意味はこう
do x <- m
   do y <- f x
      g y

==
-- 規則3の右側
do y <- do x <- m
           f x
   g y

当たり前と言えば当たり前です。

でも、こうじゃないと整合性が取れない例を見せてくれないと、必要性が理解できません。。。