具体的な値でモナド則を確認する - Maybe編

モナド則に具体的な値をいれて理解を深めてみましょう。
今回はMaybeモナドを使ってみます。

モナド則

モナド則を確認しておきましょう。

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

Maybeの実装

Maybeモナドの実装を確認しておきます。

return x = Just x

x >>= f = case x of
  Just y -> f y
  Nothing -> Nothing

モナド則に具体的な値をいれてみよう

return x >>= f == f x

xが1の場合

左辺

return x >>= f

-- xは1である
return 1 >>= f

-- return を適用
Just 1 >>= f

-- >>= を適用
case (Just 1) of
  Just y -> f y
  Noting -> Nothing

-- Just yにマッチするので
f 1

右辺

f x

-- x は1である
f 1

右辺と左辺が一致した

まとめ

関数fに使う値をreturnしてから使うのと、そのまま使っても結果は変わらないことがかくにんできました。returnした値にfを使う方法が>>=と読めそうですね。

m >>= return == m

mが Just 1の場合

左辺

m >>= return

-- m はJust 1である
Just 1 >>= return

-- >>= を適用
case (Just 1) of
  Just y -> return y
  Nothing -> Nothing

-- caseを処理する。 Just y にマッチする
return 1

-- returnを適用
Just 1

右辺

m

-- mはJust 1である
Just 1

mが Nothingの場合

右辺

m >>= return

-- mはNothingである
Nothing >>= return

-- >>= を適用
case Nothing of
  Just y -> return y
  Nothing -> Nothing

--- caseを処理する。Nothingにマッチする
Nothing

左辺

m

-- mはNothingでらう
Nothing

左辺と右辺が一致した。

まとめ

returnを使っても値が変化しないことが確認できました。

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

m が Just 1の場合

左辺

(m >>= f) >>= g

-- m は Just 1である
(Just 1 >>= f) >>= g

-- 左の >>= を適用
(case Just 1 of
  Just y -> f y
  Nothing -> Nothing) >>= g

-- caseを処理する。Just y にマッチする
f 1 >>= g

右辺

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

-- m は Just 1 である
Just 1 >>= (\x -> f x >>= g)

-- >>= を適用
case Just 1 of
  Just y -> (\x -> f x >>= g) y
  Nothing -> Nothing

-- caseを処理。 Just y にマッチする
(\x -> f x >>= g) 1

-- ラムダ式を処理する
f 1 >>= g

左辺に一致した

m が Nothingの場合

左辺

(m >>= f) >>= g

-- m はNothingである
(Nothing >>= f) >>= g

-- 左の >>= を適用
(case Just 1 of
  Just y -> f y
  Nothing -> Nothing) >>= g

-- caseを処理する。Nothing にマッチする
Nothing >>= g

-- >>= を適用
case Nothing of
  Just y -> f y
  Nothing -> Nothing

-- caseを処理する。Nothingにマッチする
Nothing

右辺

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

-- mはNothingである
Nothing >>= (\x -> f x >>= g)

-- >>= を適用
case Nothing of
  Just y -> (\x -> f x >>= g)
  Nothing -> Nothing

--- caseを処理する。Nothingにマッチする
Nothing

右辺と左辺が一致した

まとめ

どちらの>>=を先につかっても結果が一致することが確認できました。

最後のまとめ

モナド則は >>= と return の性質を説明しているのに過ぎません。
>>= は m a を a -> m a という型の関数と組み合せて使えるようにする演算子です。
return はもっとも基本的な a -> m aです。

第１法則は return x >>= f == f x >>= return と書くと交換法則のようにみえますね
第２法則は returnが単位元のようにみえますね。
第３法則は どちらの>>=を先に計算しても結果が一致する結合法則のようにみえますね。

ところで、登場した値は m aと a -> m a です。 a -> m a な値に、m aを使うとaをおきかえて m a -> m (m a) になります。m (m a)という型が登場していますが、モナド則に現れません。>>=をつかって a -> m aを使うと m (m a)にならず、m aのままになるのがポイントです。