今年(2009)の4月に書いたエントリー「予告:セミナー「モナド」シリーズを開始します」の後半で、「さて、僕のモチベーションの由来として、…」ということで、2005年3月28日に書いたエントリー「圏論とコンピューティング・サイエンス(とか勢いで書いてみる)」を全文引用しています。もう一度引用はしませんが、僕が“隠れカテゴリスト”だった状況が書いてあります。
実際、1990年代後半くらいから僕は、コンピューティングとソフトウェアを理解する手段として、システムを設計するガイドラインとして圏論を使っています。万能だとも最強だとも言いませんが、「かなり役に立つ」とは言えます。
ただ、せっかく圏論を学んでも使い方が間違っているような、それじゃうまくいきっこないじゃん、みたいな状況もあるようです。ラムダセミナー、モニャドセミナー、コモニャドセミナーをやってみて驚き、強く印象に残ったことは、学校で習った「集合と写像」の刷り込みがよほど強いのか、皆さん、計算現象も集合と写像で考えようとしちゃうことです。…… それはダメですよ。その発想をやめないとラチあかんて。
その他にも、既存の理論や典型的事例、特定のプログラミング言語からの類推/思い込み/先入観などが、圏論の実際的な応用に対して障害/障壁になっているようです。一朝一夕に、これらの“邪念”を追い払うことはできそうにないですが、思いついたヒントをパラパラと述べてみます。あっ、エントリー・タイトルは大仰でした。すんません。
内容:
計算は関数ではない
まず最初に断っておくと、集合と写像の概念が不要とかダメだと言う気はありません。それどころか、圏論でも外側の枠組みとしては(多くの場合*1)集合と写像をヘビーに使っています。ですが、対象は集合とは限らないし、射が写像とは限らないってことです。圏論は圏論であって、集合と写像の理論ではありません。
データ型は対象で、計算は射でモデル化できます -- そう言っていいでしょう。しかしこれは、データ型が集合で、射が写像だと言ってるんじゃありません。仮に射が写像であったとしても、その写像の集合論的な始域/終域が、射の域/余域を与えるとは限りません。写像とみなして同じ計算でも、計算そのものとしては異なるかもしれないし、その逆のケースもあるでしょう。
ましてや、特定のプログラミング言語のなかで「関数」とか「メソッド」とか呼ばれているものが、素直に射に対応しているなんてことは滅多にありません。もちろん、プログラミング言語の計算単位が射に対応してくれれば美しいし、嬉しいですが、世の中そんなにうまくいかんのよ。
仮に、とあるプログラミング言語の関数が射でモデル化できるとしても、引数の型が域で、戻り値の型が余域か? というと、そんなことも滅多にありません。その関数と呼ばれる計算単位が、非ローカル変数を参照/更新しているかもしれません。ファイルIOやデータベースアクセスやネットワーク通信もしているかもしれません。また、後述するように、引数の一部は入力じゃなくてインデックスかもしれません。
数学やプログラミング言語で、たまたま「関数」と呼ばれているナニモノカを、そのまま射だと思い込むのは、あまりに(悪い意味で)ナイーブに過ぎます。その発想が通じるのは、オモチャの例題だけです。
- 参考:偏見、誤解、曲解など
モナド登場
非ローカル変数、状態、外部ストレージへのアクセスなどを、圏論的にうまく扱う方法にモナドがあります。“不純”(副作用あり)だと思われている計算を扱うにはモナドは必須です。
「俺の使っているプログラミング言語にはモナドがないから…」なんてのはモナドを使わない理由になりません。C言語の標準ライブラリにハッシュマップがない(よね? 今でも)から、ハッシュマップを使ったプログラミングはC言語では無理、なんて言い訳しますか。
例えば、http://d.hatena.ne.jp/m-hiyama-memo/19990801/1249450075 を見てください。モナドの例にタートルグラフィックスを出して、そのサンプルをJavaScriptで書いてます(オモチャですけど)。JavaScriptの言語機能にモナドがあるわけじゃないです。
モナドでは不十分
モナドとそのクライスリ圏は、不純な計算の解釈に対して、とてもうまく働きます。しかし、「アクセス権限チェックを、モナドとコモナドで定式化してみる」で述べたように、単一のモナドでは不十分なときが多く、コモナド、両モナドが必要になります。
複数のモナド/コモナドが登場すると、それらの(コ)モナド達の関係が問題になり、ほぼ確実にベックの法則を使うことになります。テンソル強度(tensorial strength)や線形分配性(linear distributivity)はベックの法則(分配律)の変種と考えられます。
ベックの法則の図示
もうひとつ、モナドだと痒いところがあります。モニャドセミナーのときに、田辺さんとhitotakuchanさんから同じ質問が出て、コモニャドセミナーでそれに答えたのですが、この質問が「モナドの痒いところ」に関係してました -- 曰く「モナドのアクションは、いつ誰が実行するの?」
例えば、ファイル出力モナドを使うと、実際のディスクへの書き込みがいつ実行されるかわかりません。これは、モナドのいい点であり、プログラマは「ホントの書き込み」を意識しなくて済むのです。普通のファイル出力だってキャッシュされるので、ホントの書き込みのタイミングはわかりません。
しかし、「ホントの書き込み」を制御したいこともあります。バッファフラッシュとか変更のコミットとかです。モナドだけを使っている限り、ホントの書き込みを見たり制御したりはできません。
モナド概念を少し拡張すると、バッファフラッシュとかコミットまで取り込むことができます。拡張されたモナド概念をなんと呼ぶか僕は知らないのですが、線形代数の加群に対応します(モナドは多元環に対応します)。しょうがないのでモナド加群とでも呼ぶことにして; このモナド加群を使うと、モナドが状態空間に作用して、最終的に状態遷移を引き起こすところまで細かく制御できます*2。
関数と射:再論
射が計算のとき、計算の入力が域で、出力が余域と考えるのはいいでしょう。もちろん、大域変数とかファイルとかの不純な入出力も考慮します。たまたま(あくまでたまたま)、プログラミング言語の関数が計算の射に対応しているとき、引数は入力の一部、戻り値は出力の一部と考えていいのでしょうか?
ほとんどのケースで、戻り値は出力の一部になりますが、引数を入力に勘定しないことはしばしばあります。総称関数の型パラメータは、入力というよりは射を特定するインデックスとして働きます。型パラメータじゃなくても、引数により射を特定することはあります。
可変引数の足し算 sum(int, int...) を考えると、引数の個数で射が特定されます*3。sumという名前は、たくさんの射を束ねたものに付けられた名前です。第一引数で、加減乗除のどれを実行するかを示す calc(enum {ADD, MUL, SUB, DIV}, int, int) という関数の場合は、add, mul, sub, div という4つの計算を便宜上束ねたとみなすほうが自然かもしれません。
別な問題として、プログラミング言語の関数が、射とみなすには粒度が適切じゃないことがあります。例えば、大域変数を読み書きする不純関数があったとき、書き込みをしたタイミングで計算を分割したほうが考えやすくなります*4。このときは、1つの関数を“複数の射の結合”としてモデル化することになります。逆に、複数の関数を集約して1つの射と考えることもあるでしょう。
こんなことは言いたくないのだけど
ラムダセミナーで使った資料 http://www.chimaira.org/archive/slide20090124-1s.pdf の8ページ目に次のような断り書きがあります。
なんでこんな注意が必要なのか? まったくもって忸怩<じくじ>たる思いがするのですが、僕としては口に出したくない恥ずかしいセリフを言わざるをえないからです。そのセリフとは例えば:
- その執着をふり払いなさい。そうすれば、新しい世界が見えるはずです。
学校教育とプログラミング言語の刷り込みと呪縛は、実に強烈なもので、視点・視角をガッチリと固定化する働きを持つようです。圏論も同様に、新しい呪縛になり得るのかもしれません*5が、学校教育とプログラミング言語からの視点・視角を一旦は破壊しないと新しい呪縛に身をゆだねることもままならないのは確かなようです。