このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

モナドの定義とか

モナド関係で、KMさんと酒井さんにコメントをいただいて、僕もコメント欄に書き込みました。話が少しややこしくなったので、このエントリーで続きを。

コメント欄のやりとりで分かったことは、“Haskellモナド”がモナドもどきではなくて、どうも、正真正銘の圏論モナドであるらしいことです。であれば、Haskell知らずの僕が語ってもまー大丈夫かな、と。(メモ編に書くべき内容かもしれないけど。)

Listは典型的モナドに思えないかも知れない

「Listモナドは典型的モナドだ」と僕は書いたのだけど、Haskellのヒトには違和感あるかもしれないですね -- Listはたいていのプログラミング言語でサポートされている平凡なデータ構造ですから。状態遷移とか入出力のような副作用を表現するモナドのほうが“モナドらしい”のでしょう、おそらく(憶測モード)。そうであってもなお、Listがやっぱり典型例なのは事実なので、主にListの例で話をします。

そのListの例で僕は、flattenとsingletonという関数を主役にしたのですが、Haskellでは「>>=」という演算子が基本のようです(singletonとreturnは同じ)。flattenと>>=は、相互に相手を定義可能なので、どちらを基本に採用するかは好みの問題です。もっとも、プログラミングでは>>=のほうが扱いやすいと感じる人が多いみたいですが。

記号法と定義法を整理する

用語や記号法の流儀がいろいろあるので、ちょっとまとめておきます。Mはモナド(Listだと思ってもよい)だとします。正確には、Mはモナドを構成する一部品に過ぎませんが、気にしない方向で。

概念の名称 圏論(の多数派)の記法 (一部の)プログラミング言語の記法
関数適用 f(a) f(a), f a
型パラメータ、対象 X X, x
XからYへの関数(射) f:X→Y Y f(X a), f:: x -> y
型構成子(の結果)、関手の対象部分 M(X) M, M x
持ち上げ、関手の射部分 M(f), f* map(f), fmap(f), lift(f)
モナド乗法 μ flatten, join, union, concat
モナド単位 η singleton, unit, return
拡張 f#, f^, f* f =<<, (>>= f)

[追記 date="20060422"]拡張に対応する記号「>>=」「=<<」に関しては、「さらに『モナド入門』に補足:記号だの図だの」に書きました。[/追記]

モナドの定義法の代表的なものとして、代数的な(一種のモノイドとみなす)スタイルと、拡張(extension)を使うスタイルの2つがあります。上の表にあげた概念のなかで、(型構成子, 持ち上げ, モナド乗法, モナド単位)を使って定義するのが代数スタイル、(型構成子, モナド単位, 拡張)を使うのが拡張スタイルです。(型構成子, モナド単位, 拡張)の3つ組はKleisliトリプルと呼ばれます(昔は、モナドのことを単にトリプルと呼んでいたりした)。

2つのスタイルの定義と、それらが同値であることを以下で説明しますが、次の記法を使うことにします(Listの例にだいたいあわせる)。

  • 関数適用 -- f(x)
  • 型パラメータ -- X
  • XからYへの関数 -- f:X→Y
  • 型構成子(の結果) -- M(X)
  • 持ち上げ -- f*
  • モナド乗法 -- flatten
  • モナド単位 -- singleton
  • 拡張 -- f^
  • 拡張+適用 -- >>= (二項中置演算子とみなす)

それと、関数結合(合成)は、f;gとg・fの両方を使います。idは恒等関数です。

拡張(extension)スタイルによるモナドの定義

(型構成子, モナド単位, 拡張)の3つ組を(M, singleton, ^)とすると、singletonはXごとに singleton_X:X→M(X) の関数を与えます。曖昧性がなければ「_X」は省略します。f:X→M(Y)に対して、fの拡張f^:M(X)→M(Y)が決まりますが、事情は同様で; ext(f) = f^ とすれば、このextもXごとにext_X(f)と記すべきですが、「_X」を省略してもたいてい大丈夫です。

singletonと^(拡張)に関する法則は次のとおり(x∈X、m∈M(X)):

  1. singleton:X→M(X)に対して、singleton^:M(X)→M(X)は恒等関数;i.e. singleton^(m) = m。
  2. singleton:X→M(X)、f:X→M(Y)に対して、(singleton;f^):X→M(Y)はfと同じ;i.e. f^(singleton(x)) = f(x)。
  3. f:X→M(Y)、g:Y→M(Z)に対して、(f;g^)^ = f^;g^;i.e. (g^・f)^(m) = (g^・f^)(m)。

Haskellの>>=は、(m>>= f) = f^(m) なので、次の形に書き換えられます。「=」は普通の等号です。

  1. singleton^(m)は (m>>= return) だから;(m>>= return ) = m。
  2. f^(singleton(x))は ((return x) >>= f) だから;((return x) >>= f) = f x。
  3. (g^・f)^(m)は、(m >>= g^・f)、そして g^・f = λx.(f(x) >>= g)。また、(g^・f^)(m) = g^(f^(m)) = (m >>= f) >>= g だから; m >>= (\x -> (f x >>= g) = (m >>= f) >>= g。

演算子>>=をextApplyとでも書くと:

extApply(m, f) = apply(ext(f), m) = ext(f)(m)
ext(f) = λm.(extApply(m, f))

なので、ext(記号^)とextApply(記号>>=)がお互いに相手を定義できることが分かります。

代数スタイルの定義

(型構成子, 持ち上げ, モナド乗法, モナド単位)の4つ組を(M, *, flatten, singleton)とします。すると、まずMと*に関して次の法則が必要です。

  1. (f;g)* = f*;g* ;i.e. (g・f)*(x) = g*(f*(x))。
  2. id* = id ;i.e. id*(m) = m。

アスタリスク「*」が上付きに見えるかも知れませんが、僕の気持ちとしては下付きアスタです。

さらに、singletonとflattenに関して次が要請されます(m∈M(X)、mm∈M(M(X))):

  1. flatten(flatten(mm)) = flatten(flatten*(mm))
  2. flatten(singleton(m)) = m
  3. flatten(singleton*(m)) = m

拡張を使うスタイルと代数スタイルの定義が等価であることは、計算で示せます。

計算してみる

拡張スタイルでの法則を次の形に書いておきます。

  1. singleton^ = id
  2. singleton;f^ = f
  3. (f;g^)^ = f^;g^

これらを仮定して、次を示します。

  1. (f;g)* = f*;g*
  2. id* = id
  3. flatten;flatten = flatten*;flatten
  4. singleton;flatten = id
  5. singleton*;flatten = id

[追記]行きがかり上、flatten, singletonなんて長い関数名を使ってますが、実際に手で計算するときは、短い名前(例えば、muとeとか)を使うことをお勧めします。長いとtypoばかりする。[/追記]

まず、id:M(X)→M(X)、f:X→Yに対して、次のように定義します。

flatten = id^ : M(M(X))→M(X)
f* = (f;singleton)^ : M(X)→M(Y)

あとはワシャワシャ計算するのみ:
[追記]flatten*;flattenの計算が間違っていた(失礼しました)。訂正のついでに、右側のコメントに、次の行への変形の根拠を書きました。[/追記]

  f*;g*                               // *の定義
= (f;singleton)^;(g;singleton)^       // 3.
= ((f;singleton);(g;singleton)^)^     // ;の結合律
= (f;(singleton;(g;singleton)^))^     // 2.
= (f;(g;singleton))^                  // ;の結合律
= ((f;g);singleton)^                  // *の定義
= (f;g)*
  id*             // *の定義
= (id;singleton)^ // idの性質
= sigleton^       // 1.
= id
  flatten;fletten // flattenの定義
= id^;id^         // 3.
= (id;id^)^       // idの性質
= (id^)^

  flatten*;flatten       // flattenの定義
= (id^)*;id^             // *の定義
= (id^;singleton)^;id^   // 3.
= ((id^;singleton);id^)^ // ;の結合律
= (id^;(singleton;id^))^ // 2.
= (id^;id)^              // idの性質
= (id^)^
  singleton;flatten // flattenの定義
= singleton;id^     // 2.
= id
  singleton*;flatten            // flattenの定義
= signleton*;id^                // *の定義
= (singleton;singleton)^;id^    // 3.
= ((singleton;singleton);id^)^  // ;の結合律
= (singleton;(singleton;id^))^  // 2.
= (singleton;id)^               // idの性質
= singleton^                    // 1.
= id

リストの例を使えば、具体的に手で触って確認できます。逆向きは、次の定義のもとでまたワシャワシャ計算します。

 f^ = f*;flatten