Haskellにおけるモナド

Haskell Monad

こんばんは、south37です。

前回は「圏論」におけるモナドについて触れた訳ですが、今回はいよいよモナドがどういう風にHaskell上で表現されているかに迫ってみたいと思います。

Haskell における Monad

自己関手であるモナド

前回、「モナド」は「自己関手」であると述べました。ここで、そもそも「関手」がHaskellにおいてどのように表現されていたかを思い出してみましょう。

まず、Haskellにおいては、「型」を「対象」として「関数」を「射」とするような「圏」を考えます。Haskellにおける「全ての型」が「対象」であるような「圏」はHaskと呼ばれ、その部分圏としてリスト型のみを「対象」とするLstなどが存在します。

関手は「圏」から「圏」への対応付けを行う訳ですが、それは「対象」を写す「対象関数」と、「射」を写す「射関数」の組み合わせと考える事が出来ます。Haskellにおいては、関手はFunctor型クラスとして表現されており、fmapという「射関数」に対応する関数が存在します。

例えば、HaskをLstへうつす場合を考えてみます。a型から[a]型を作るのは簡単で、ただリストの中に入れるだけです。その際、例えばf :: a -> bという関数fが存在したとすると、fmap fの型は[a] -> [b]となります。すなわち、fmapをfに作用させる事によって、a,bというHaskの「対象」同士を結びつける「射」であったfが、[a],[b]というLstの「対象」同士を結びつけるfmap fという「射」へと写された訳です。fmapがまさに「射関数」の働きをしている事が分かります。

上記の例ではHaskからLstへの「関手」を考えた訳ですが、HaskからHaskへの関手も考える事が出来ます。こういった関手は、同じ圏への「関手」である為、「自己関手」と呼ぶ事が出来ます。HaskellにおけるMonadも、HaskからHaskへの「自己関手」となっています。

Monad 型クラス

Haskellにおけるモナドは、以下の様に型クラスとして定義されています。

class Monad m where
  return :: a -> m a
  
  (>>=) :: m a -> (a -> m b) -> m b
  
  (>>) :: m a -> m b -> m b
  x >> y = x >>= ¥_ -> y

  fail :: String -> m a
  fail msg = error msg

class a where ~という構文は、型クラスを定義する時に使われます。上記のコードはMonadという型クラスに属する型であるmが、return、>>=、>>、failなどの関数の定義を必要とする事を示しています。

「モナド」であるような型とは、リスト型やMaybe a型やIO a型などです。これらの型はみなMonad型クラスに属しており、returnや>>=が定義されています。さらには、>>=や>>の糖衣構文である「do構文」が使える様になっています。「do構文」の詳細については、後々詳しく触れたいと思います。

「モナド」としての振る舞いを考える上では、>>=から自明な実装が与えられるjoinと、returnが重要になります。

join :: Monad m => m (m a) -> m a
join x = x >>= id

returnとjoinに着目してその型を見てみると、return :: a -> m aやjoin :: m (m a) -> m aのようにaの前につくmの数を増やしたり減らしたりしている事が分かります。実は、これらは前回紹介した自然変換η: I -> Mやμ:M ◦ M -> Mに対応しています。

それぞれ、詳しく見て行きましょう。

return

returnは自然変換η: I -> Mに対応する関数です。

恒等関手iがaに適用された状態をi aと表現すると、aとi aは同じである為returnの型はi a -> m aと表現する事が出来ます。こういったイメージを持つと、returnはiをmへうつす役割をしているように見えてきます。これはまさしく、η: I -> Mの振る舞いと言えますよね！！

join

joinは自然変換μ:M ◦ M -> Mに対応する関数です。その型はm (m a) -> m aであり、μがM(M(X)) -> M(X)とも表現出来る事を考えると、まさしくμの振る舞いに対応している事が分かります。

returnやjoinは「自然変換」に対応する為、「射の構造」、すなわち射の合成を保ちながら変換を行う必要があります。この条件は、次で紹介する Monad則 に含まれています。

Monad則

wikibooksのhaskellのページにおいて、モナドが従わなければならない4つの公理が紹介されています。これらは、 Monad則と呼ばれています。

モナド M : C -> C と、A, B ∈ Cに射 f : A -> B があるとする。 このとき次が成り立たなくてはならない。

1. join ◦ M(join) = join ◦ join
2. join ◦ M(unit) = join ◦ unit = id
3. unit ◦ f = M(f) ◦ unit
4. join ◦ M(M(f)) = M(f) ◦ join

Haskellの言葉を用いて(returnやjoin、fmapを用いて)書き直すと、以下の様になります。

1. join . fmap join = join . join
2. join . fmap return = join . return = id
3. return . f = fmap f . return
4. join . fmap (fmap f) = fmap f . join

上記のうち最初の1と2は、前回紹介したモナドが従わなければならない規則の1と2にそれぞれ対応しています。すなわち、「結合則」に対応する公理と、「単位元の存在」に対応する公理という訳です。

3は、returnがちゃんと自然変換となっている事の証明です。 両辺ともに、型はa -> m aとなっています。returnを作用させてもちゃんと構造が保存されている為に、恒等関手によってうつされた射fをaに適用したものが、モナドMが適用されたものにfmap fを適用する場合と対応する(f aにreturnを適用する事で一致する)ことを意味しています。 つまり、恒等関手とモナドMの間で「射の構造」を保存出来ている事を表しています。

4が、joinがちゃんと自然変換となっている事の証明です。 型は、両辺ともにm (m a) -> m aです。すなわち、m ◦ mを適用したものと、mを適用したものとの間で射の対応関係がついてる事を表しています。 f :: a -> bという関数を考えると、m (m a)を受け取ってm (m b)を返す射がfmap (fmap f)であり、公理4はそれがfmap f :: m a -> m bに対応する事を表します。 右辺では、m (m a)をjoinによってm aに写しており、そこにfmap fを適用する事がm (m a)にfmap (fmap f))を適用する場合と対応する(joinする事で一致する)というのがこの式の意味するところです。 すなわち、M ◦ MとMの間で射の構造が保存出来ている事を表しています。

うん、オーケーですね！！

とりあえずのまとめ

Haskellにおけるモナドは、Monad型クラスとして表現されており、ηに対応するreturnとμに対応するjoinの定義が必要とされる事が分かりました。また、モナドのモノイド的性質やηやμの自然変換としての性質を満たす為に、Monad則というものを満たす形でreturnやjoinを定義しなければならない事が分かりました。

次回は、do構文とMonadの関係を見て行きたいと思います。

どうでも良い話

今日はちょっと余裕が無くて、おざなりな説明になってしまいました。申し訳ありません。時間が出来次第、適宜分かり易い説明に書き換えて行ければいいと思っています。

あと、Monad則の1と2について説明を省きましたが、前回載せていた図式と見比べながらモナド則の式を見つめていると、何となく何をやっているのかイメージ出来ると思います。お暇があればやってみて下さい。 Monad則に関しては、joinでなく>>=を使って書く事も出来るようです。すごいHaskellたのしく学ぼうにはそちらが紹介されていました。まだ自分の中でjoin版と>>=版の対応付けが出来てないのですが、それも理解したらまとめてみたいです。

>>=の読み方はバインドというそうです。何でそんな呼び方をするかについては、「do構文」の説明のところで一緒に説明出来たらいいと思います。ヒントは、「do構文」で使うa <- Maybe "Hello"みたいな構文です。

すごいHaskellたのしく学ぼう!

すごいHaskellたのしく学ぼう!