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

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

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

参照用 記事

コモナドは何の役に立つ

モナドは、部分関数、非決定性関数、例外(エラー)、コレクション・データ型など、純粋関数計算の不純な(?)拡張を記述するために使えます。なかでも分かりやすいのは、副作用への応用でしょう。ここで言う副作用とは、大域変数への代入、ファイルIO、データベースへのアクセス、画面描画(グラフィックス)、状態を持つ計算などです。

モナド圏論的に定式化して、その双対を取るとモナドという概念になります。モナドに比べてコモナドは地味で注目される機会が少ないのですが、コモナドも純粋関数計算を拡張する手段を与えます。

実際には、副作用を表現するモナドと一緒に、たいていはコモナドも出てきているのですが、ちょっと影が薄いんですよね。ここでは、読み取り専用大域変数(イミュータブルな環境)への参照がコモナドになっていることを紹介します。

大域変数の参照

大域変数への代入(書き込み)は、モノイドのスタンピングモナドで記述できます。このことは、「単一代入のモノイド、スタンピングモナド、モナド工場」「モノイドからモナドを作る」で述べました。

大域変数を参照(読み取り)はするが、書き込みをしないような関数を考えてみます。次はそのような例です。

function increment(x) {
  return x + a;
}

「クロージャとラムダ式は同義だ、と主張してみる」で話題にした so-called“クロージャ”のコード(自由変数を持つ式)部分だと思ってもいいでしょう。

上のincrement関数は、引数と戻り値だけに注目すれば、Integer→Integer の関数です。あっ、JavaScriptなんで型宣言はなかったですね。ここで、Integer→Integer だと約束します。このことは、increment:Integer→Integer と書けます。

しかし、increment内で大域変数aの値を使っているので、引数xの値が決まっても戻り値が一意的に計算できるわけではありません。これは、「引数の値だけから、戻り値が計算できる」という条件を破っているので、increment関数は純粋関数とは言えません。どこか不純です。

大域変数aの型もIntegerですから、aも引数のようにみなして、increment:Integer, Integer→Integer と考えれば、incrementを純粋関数のように扱えます。最初のIntegerが隠れた引数としてのaの値、ニ番目のIntegerがxの値だとします。実は順番はどうでもよいのですが、順番を決めないと話が先に進まないので、一番目が大域変数aからの値としたのです。

余クライスリ結合

一般に、f:X→Y という関数があって、f内部で参照している大域変数aの値の型がVのとき、f':V×X→Y は、fの引数を増やして純関数だとみなしたモノだとします。g:Y→Z も同じ大域変数aを参照しているとすると、g':V×Y→Z が、gに対応する純関数です。以下で、中括弧を使った表現は、let式、あるいはLispのprognのようなもんです(ラムダ式をご存知の方はラムダ式に書き直したほうがわかりやすいでしょう)。

  • f'(v, x) = {a=v; f(x)} :V×X→Y
  • g'(w, y) = {a=w; g(y)} :V×Y→Z

このままでは f';g' が作れませんが、f'' = V×f として f'':V×V×X→V×Y を作れば、f'';g' を定義できます。V×f は idV×f の略記です。詳しくは「モノイドからモナドを作る」を参照しください。

以下は露骨な定義:

  • f''(u, v, x) = (u, {a=v; f(x)}) :V×V×X→V×Y
  • g'(w, y) = {a=w; g(y)} :V×Y→Z

f'';g' は次のように計算されます。

   (f'';g')(u, v, x)
 = g'(f''(u, v, x))
 = g'(u, {a=v; f(x)})
 = {y = {a=v; f(x)}; a = u; g(y)}

変数aは、参照されるだけで書き換えは起きてないので、上の計算で v = u です。念のため、v = u を仮定した計算をもう一度書くと:

   (f'';g')(v, v, x)
 = g'(f''(v, v, x))
 = g'(v, {a=v; f(x)})
 = {y = {a=v; f(x)}; a = v; g(y)}
 = {a = v; y = f(x); g(y)}

関数 d:V→V×V を、d(v) = (v, v) と定義しておきます。入れ子のタプルのことをうるさく言わなければ、(d×X);f'';g' は、V×X→Z という関数になっています。(d×X);f'';g' が、 f'とg'の余クライスリ結合と呼ばれる結合(合成)になっています。余クライスリ結合を表す良い記号が思いつかないので、不適切なことは承知で「$」を使うとして、f'$g' = (d×X);f'';g' 。中括弧(let式、progn)を使って書き表すと:

   (f'$g')(v, x)
 = ((d×X);f'';g')(v, x)
 = g'(f''((d×X)(v, x)))
 = g'(f''(d(v), x))
 = g'(f''(v, v, x))
 = g'(v, {a=v; f(x)})
 = {y = {a=v; f(x)}; a = v; g(y)}
 = {a = v; y = f(x); g(y)}

モナドから作る余クライスリ圏

なーんかチマチマした計算をしてきたので、ここらで圏論を使って一気に定式化しましょう。

集合Vを固定して、F(X) = V×X、F(f:X→Y) = (V×f:V×X→V×Y) として関手F:SetSetを定義します。Fは、左からの直積掛け算関手です。d:V→V×V は先に定義したとおり d(v) = (v, v) だとして、d×X を ξX:V×X→V×V×X と書きます。V×X をF(X)、V×V×X = V×(V×X) を F(F(X)) とみなせば、ξはFからFFへの自然変換になっています。ξ::F⇒FF:SetSet ですね。

1 = {*} を単元集合、e:V→1 は一意的に決まる写像として、ρX:F(X)→X を、ρX = e×X :V×X→1×X=X として定義します。1×X=X の部分は、(*, x) と x を同一視する操作です。Iを恒等関手として、ρは F⇒I という自然変換になっています。ρ::F⇒I:SetSet です。

(F, ξ::F⇒FF, ρ::F⇒I)の3つ組を考えると、これらは、結合律の双対である余結合律、単位律の双対である余単位律を満たします(確認はタルーーイ計算、だが体で理解したいなら我慢してやる)。

F(X)→Y という形の写像が余クライスリ射です。F(X)→Y の射と F(Y)→Z の射を結合するために、FF(X)→F(Y) をいったん作ってから結合して、得られた FF(X)→Z の射にξX:F(X)→FF(X) をプレ結合するのが余クライスリ結合です。クライスリ結合と完全に双対になっています。

結局、読み取り専用の大域変数を参照しながらの計算が、コモナドと余クライスリ圏で定式化できるということです。しかし、これはヤッパリ地味な話ですよね。なにもコモナドなんて持ち出さなくなっていいんじゃないの? という気はします。しかし往々にして圏論では、ほんとにツマラナイと思える事例が、極めて重要な役割を演じていたり、深い構造の入り口だったりします。

大域変数に書き込む行為(代入です)がモナドとなり、読み取る行為がコモナドだとすると、より一般に「読み/書き」行為はコモナドモナドのペアで表現されると予想できます。ファイルシステムにしろデータベースにしろ「読み/書き」行為なので、これらはコモナドモナド・ペアで定式化するのが適切かも知れません。

実例を調べると、単なるコモナドモナド・ペアがあるだけでは不十分で、コモナドモナドが一定の法則を満たす必要があります。僕は、その「法則」の形がハッキリとはわかんなかったのですが、ここ2,3日当たりを付けていたらだいたい予想できました。予想が事実だとわかったら、また報告することにします。