このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

モニャドセミナー4の予定:トランザクション計算のフレームワークとか

「モニャドセミナー4の予定:トランザクション計算のフレームワークとか」「モニャドセミナー4の予定:訂正と補足」を集約して、わずかに変更。


実務者のための圏論モナド -- つう感じで

練習、質疑応答、議論を強調したいので、スライド利用講義風のスタイルはたぶん止めます。その代わり、印刷した資料*1を配付します。お絵描き&計算用のノートと筆記具は必須です。ホワイトボード2枚メイッパイ使うでしょう。[追記 date="当日"]ホワイトボード2枚は使えないようです…(泣く)。[/追記]

「クライスリ圏の話をするぞ」という予告は守るつもりです。が、今回は次のような疑問や疑念に応えることを主眼にしたいと思います。

  • こんなことを知って、なんか実務に役に立つの?
  • 絵算はどう使うの、ホントにありがたみがあるの?

実務上の煩雑さは削り落としますが、それでも単純すぎずリアリティが残る素材として、表題のような、トランザクション計算*2を組み合わせて実行するためのフレームワークを例題にします。処理が失敗した後のロールバック処理まで考えるのは面倒なので、それは割愛; 失敗に備えて、もとのデータを残したりロギングをするメカニズムを考えるのです。この題材は、今僕が興味を持っているトピックに近いものです。こういう話のほうがリアリティとかライブ感が出るのではないか、という目論見&魂胆です。

キュー&コミット・スタイルのトランザクション計算

取り扱う例題をここで紹介しておきます。

次のような状況を考えます; 計算処理(コンピュテーション)をする際に、外部環境(非ローカル変数、ファイル、データベースなど)を参照すること(読み取り)は自由にできるが、外部環境を直接変更することは許されてないとします。その代わり、当該の計算処理が完了したときに実行される予定の更新リクエストを発行できます。リクエストは発行順序を保ってキューに貯えられます*3。計算処理が無事に終わると、キューイングされた更新リクエストが順に実行され、外部環境は変更されます -- 正確に言うと、あたかも変更されたように振る舞います。

以上のような処理に対して、外部環境は暗黙に与えられますが、処理ごとに明示的に渡すパラメータがあってもかまいません。また、計算結果は戻り値として返せます。環境の更新は副作用と考えられます。2つの計算処理をつないだものをトランザクションとみなす場合を考えると、1つめの処理の直後でホントに環境に変更を加えると、2つ目の処理が失敗したときに初期状態を復元できないかもしれません。実際のコミットは、計算処理全体がホントに終わったときに行うべきで、部分計算に対するコミットは仮のコミットとなります。

ひとつ注意しておくと、「直接に外部環境を変更することは許されてない」というのは、外から見たときの話で、計算処理を実行する主体*4は「許されている/許されてない」などを知っているわけじゃありません。リクエスト発行を変更と認識しても問題はありません。ただ、変更しても参照している元データへの即時反映が行われない点には注意が必要ですけども。

圏論モナドをどう使うのか

副作用としての書き込み(メモリ/ストレージの更新)はモノイダル・スタンピング・モナドで定式化して、外部環境の参照(読み取り)は、その双対であるコモノイダル・スタンピング・コモナドを使って定式化します。書き込みのコミット操作は、モノイド作用(線形代数の用語では加群)で定式化します。計算処理の逐次実行は、クライスリ結合、余クライスリ結合、両クライスリ結合となります。

[追記]以下の段落で「半関手」という言葉はまったく不適切でした。訂正と補足をご覧ください。[/追記]

クライスリ圏、余クライスリ圏、両クライスリ圏の計算では、ラッピング半関手対応を使う方法を紹介しましょう。半関手(semi-functor)とは、結合は保存するが恒等の保存が保証されない対応です。「ラッピング」は僕がでっち上げた形容詞ですが、Adapterデザインパターンとか、あんな感じ*5。結合機構(コンポジション・マシナリ)の一部を、射に押しつける技法ですね。ラッピング対応により、計算は(絵算も等式計算も)だいぶ楽になります。

なんか難しげ? 大丈夫、ここで絵算が威力を発揮するはず。絵に描けば難しそうな概念もクリアになります。本来、モナドの取り扱いは自然変換の計算になりますが、モノイダル・スタンピング・モナドに限れば、射の変形操作(ワイヤリング)だけでだいたい済みます。まー、モニャドセミナー3で自然変換を飛ばしちまった都合で、自然変換なしで済ませたいという事情もあります。

モノイダル・スタンピング・モナドに限定して、自然変換を正面から取り上げないことは、絵算を矮小化することになりますが、それでも絵算の威力と醍醐味はある程度は伝わるんじゃないのかなー、と思ってます。


モニャドセミナー4の予定:訂正と補足

半関手は2つの意味で不適切な言葉でした

クライスリ圏、余クライスリ圏、両クライスリ圏の計算では、ラッピング半関手を使う方法を紹介しましょう。半関手(semi-functor)とは、結合は保存するが恒等の保存が保証されない対応です。「ラッピング」は僕がでっち上げた形容詞ですが、Adapterデザインパターンとか、あんな感じ。結合機構(コンポジション・マシナリ)の一部を、射に押しつける技法ですね。ラッピング半関手により、計算は(絵算も等式計算も)だいぶ楽になります。

半関手という言葉は使うべきじゃなかったです。「結合は保存するが恒等の保存が保証されない対応」という定義はいいのですが、「F:C→D が半関手だ」というときは、CとDが圏、少なくとも半圏(圏から恒等を除いた構造)であることが前提となります。

僕が想定している状況では、Dは圏だけど、Cが何であるか全然不明なんです。Cが圏であることも、半圏であることも保証できません。この状況で半関手というのは不適切です。

Cに部分二項演算があるが、結合律さえも保証されてないとき、Cはマグマ(正確には1-マグマ*6)と呼ぶことがあります。この言葉を使うなら、ラッピングは、マグマ準同型になっている、とは言えます。僕が利用したいのは次の事実です。

  • Cがマグマ、Dが圏で、F:C→Dは単射であるマグマ準同型(演算を保った埋め込み)のとき、Cは半圏(結合律を満たすマグマ)である。事後的に、Fは半関手である。

ラッピング半関手と呼ぶのはダメですから、ラッピング対応と呼ぶことにします。

それと、「恒等の保存が保証されない」と書いてますが、ラッピング対応は実は恒等も保存するのです。恒等の保存を使う必要性がなかったので、意識してなかっただけでした。恒等(歴史的事情から反射と呼ぶ)の保存を仮定できると、次の命題がなりたちます。

  • Cが反射的マグマ、Dが圏で、F:C→Dは単射である反射的マグマ準同型のとき、Cは圏である。事後的に、Fは関手である。

反射的マグマとは、反射的グラフに二項演算が入った構造です。圏とほぼ同じ計算体系ですが、計算法則が何もないものです。

計算が簡単にならないときもある

モノイダル・スタンピング・モナドと、コモノイダル・スタンピング・コモナドから、次の圏を構成します。

  1. モナドからクライスリ圏
  2. モナドから余クライスリ圏
  3. モナド/コモナド対から両クライスリ圏
  4. 作用付きモナド/コモナド対から作用付き両クライスリ圏

最初の3つについては、ラッピング対応を使うと計算が楽になるのは確かです。ただし、何の工夫もなしにやっても大した手間ではありません。

4番目の作用付き両クライスリ圏ですが、これは、ラッピング対応を使っても全然計算が楽になりません。直接的な絵算がうまく働かない例になっているようです。しょうがないので、別な手段 -- 圏論的行列計算を使うことにします、たぶん。

圏論的行列計算は、計算手順は普通の行列計算とまったく同じですが、計算の意味論をモノイド圏のなかに取ります。ワイヤリングが複雑化しちゃったときは、直接絵算より行列計算したほうがうまく行くときもあります。

[追記]二転三転ですが、やっぱり行列計算じゃなくて、直接的な絵算を使おうかと。行列計算は、発見的手法としても雑談ネタとしても面白いのですが、今回のケースでは、実用上受け入れがたい制限を付けるか、あるいは非決定性を導入して新しい圏を構成するとか、セットアップに手間がかかるんです。時間的に無理な感じ。

レイアウトに注意して描けば、直接絵算でもまーなんとかなるかな、っと。さっき絵を描いていたら、最後の最後になって、右と左を逆にすれば良かったことに気が付きました。ウゲーー、もうウンザリ。描き直す気力がないので、余分なスワップ(左右交換)が入るけど、これでもういいことにします。[/追記]

実務上の要請と帰結

「モニャドセミナー4の予定:トランザクション計算のフレームワークとか」の冒頭で言ったとおり、今回は、「アブストラクト・ナンセンスが実務的な問題解決にどう利用できるか」ってことをデモンストレートしたいのです。その実務的観点をまとめると:

  1. プラッガブル・コンポネントとフレームワークにより、ある種のトランザクション計算(エコ計算と呼ぶのが適切?)のメカニズムを作りたい。
  2. コンポネント作成者の負担をできるだけ少なくしたい。特に、退屈なルーチンコードを書くようなことは強制しない。
  3. フレームワークの実装もできるだけ単純にしたい。既存の知識やコードで済むならそれで済ませたい。
  4. 実行される計算が、型安全であることを保証したい -- 型エラーが起きないことは実行をせずにチェックしたい。
  5. 一見矛盾するような要求を調停するために、コンポネント群の組み立てと実行に先立ち、静的または動的にラッピングをする。ラップされたコンポネント群をフレームワークの実行環境上で走らせる。

*1:カタカナだと、レジュメ、アジェンダシラバスとかいうんでしょうか。

*2:環境へのインパクトをキチンと制御して、好きなだけ汚染(破壊的変更)を遅延できるような計算なので、エコ計算と呼んだほうが実情を表しているかも。

*3:一般論で言えば、リクエストは必ずしもキューイングされる必要はなくて、なんらかの意味で累積されます。

*4:フレームワークに対してプラッガブルな何者かです。コンポネント、プロセス、タスク、エージェント、コマンド、… まーお好きなように呼んでください。

*5:Adapterパターンの別名がWrapperパターン。

*6:もっと正確には、1-グロービュラー・グラフ(1-globular graph)上のマグマです。