あどけない話

Internet technologies

関手、Applicative、Monadの法則

Monadとは、Applicativeであるデータ構造で、(>>=)演算子を提供し、それがMonad法則を満たすものである。

正確に表現するとこうなんですが、「はぁ?」っ感じですよね。「満たすべき法則」とか言われると、まったく理解できません。でも、オススメの形に持っていくための変換規則と捉えると分かりやすいのではないかというのが、この記事の主旨です。

関手

関手法則は以下の2つです:

  • 単位元id <$> x = x
  • 合成 : f <$> (g <$> x) = (f . g) <$> x

左辺が冗長な形、右辺がオススメの形です。これはいいですよね?

Applicative

Applicative法則は以下の4つです(<*>は左結合)。

  • 単位元pure id <*> x = x
  • 準同型: pure g <*> pure x = pure (g x)
  • 交換 : x <*> pure y = pure (\g -> g y) <*> x
  • 結合 : x <*> (y <*> z) = pure (.) <*> x <*> y <*> z

アプリカティブスタイルは、

pure g <*> x1 <*> x2 <*> ... <*> xn

でした(pure g <*> の部分は g <$> と書くことが多い)。Applicative法則は、アプリカティブならすべてこの形に直せることを保証する規則なのです。例として、t <*> pure s <*> (u <*> v) を変換してみましょう。

  t <*> pure s <*> (u <*> v)
(結合)
= pure (.) <*> (t <*> pure s) <*> u <*> v
(交換)
= pure (.) <*> (pure (\g -> g s) <*> t) <*> u <*> v
(結合)
= pure (.) <*> pure (.) <*> pure (\g -> g s) <*> t <*> u <*> v
(準同型)
= pure ((.)(.)) <*> pure (\g -> g s) <*> t <*> u <*> v
(準同型)
= pure ((.)(.)(\g -> g s)) <*> t <*> u <*> v

ほらね、言った通りでしょ。

Monad

Monad法則は以下の3つです(returnpure の別名):

  • 単位元return x >>= f = f x
  • 単位元mx >>= return = mx
  • 結合  : mx >>= (\x -> (f x) >>= g) = mx >>= f >>= g

二つの単位元ですが、右辺がオススメなのは分かりますよね? 右単位元は特に有用です。do の中をいろいろ書き換えていると、知らない間に、

do ...
   y <- f x
   return y

みたいな形になっていることがあります。これは冗長なので、以下のように書けということです。

do ...
   f x

結合の法則ですが、左辺は、

do y <- do x <- mx
           f x
   g y

ですから冗長ですね。一方右辺は、

do x <- mx
   do y <- f x
      g y

という意味ですが、これは平坦化できて、

do x <- mx
   y <- f x
   g y

と書けます。

すなわち、do入れ子で書かずに、平坦な形でスッキリ書いてねという意味です。

まとめ

法則は、オススメの形式が右に書かれてないことも多いので気づきにくいのですが、「オススメの形式に書き換えてよいことが保証されているよ」と理解すれば親しみ易くなりませんか?

追記

4つのApplicative法則が満たされると、 pure f <*> x = f <$> x が自動的に満たされます。

関手の単位元を示すために、f = id を代入:

  pure f <*> x
(単位元)
= pure id <*> x
= x

関手の合成を示す:

  pure f <*> (pure g <*> x)
(結合)
= pure (.) <*> pure f <*> pure g <*> x
(準同型)
= pure ((.) f) <*> pure g <*> x
(準同型)
= pure ((.) f g) <*> x
(中置表記)
= pure (f . g) <*> x

よって、2つの関手法則は満たされるので、 pure f <*> x = f <$> x です。