予定している筋書きは「モニャドセミナー4の予定:トランザクション計算のフレームワークとか」に書いたとおりで、今のところ心変わりしてません。
内容をもう少し具体化しようとしたら、案の定、僕の勘違いや早とちりがありました。当日訂正してもいいのですが、書かれたものに口頭(だけ)で訂正もマズイと思うので、ここに訂正と補足を書きます。
半関手は2つの意味で不適切な言葉でした
クライスリ圏、余クライスリ圏、両クライスリ圏の計算では、ラッピング半関手を使う方法を紹介しましょう。半関手(semi-functor)とは、結合は保存するが恒等の保存が保証されない対応です。「ラッピング」は僕がでっち上げた形容詞ですが、Adapterデザインパターンとか、あんな感じ*1。結合機構(コンポジション・マシナリ)の一部を、射に押しつける技法ですね。ラッピング半関手により、計算は(絵算も等式計算も)だいぶ楽になります。
半関手という言葉は使うべきじゃなかったです。「結合は保存するが恒等の保存が保証されない対応」という定義はいいのですが、「F:C→D が半関手だ」というときは、CとDが圏、少なくとも半圏(圏から恒等を除いた構造)であることが前提となります。
僕が想定している状況では、Dは圏だけど、Cが何であるか全然不明なんです。Cが圏であることも、半圏であることも保証できません。この状況で半関手というのは不適切です。
Cに部分二項演算があるが、結合律さえも保証されてないとき、Cはマグマ(正確には1-マグマ*2)と呼ぶことがあります。この言葉を使うなら、ラッピングは、マグマ準同型になっている、とは言えます。僕が利用したいのは次の事実です。
- Cがマグマ、Dが圏で、F:C→Dは単射であるマグマ準同型(演算を保った埋め込み)のとき、Cは半圏(結合律を満たすマグマ)である。事後的に、Fは半関手である。
ラッピング半関手と呼ぶのはダメですから、ラッピング対応と呼ぶことにします。
それと、「恒等の保存が保証されない」と書いてますが、ラッピング対応は実は恒等も保存するのです。恒等の保存を使う必要性がなかったので、意識してなかっただけでした。恒等(歴史的事情から反射と呼ぶ)の保存を仮定できると、次の命題がなりたちます。
- Cが反射的マグマ、Dが圏で、F:C→Dは単射である反射的マグマ準同型のとき、Cは圏である。事後的に、Fは関手である。
反射的マグマとは、反射的グラフに二項演算が入った構造です。圏とほぼ同じ計算体系ですが、計算法則が何もないものです。
計算が簡単にならないときもある
モノイダル・スタンピング・モナドと、コモノイダル・スタンピング・コモナドから、次の圏を構成します。
最初の3つについては、ラッピング対応を使うと計算が楽になるのは確かです。ただし、何の工夫もなしにやっても大した手間ではありません。
4番目の作用付き両クライスリ圏ですが、これは、ラッピング対応を使っても全然計算が楽になりません。直接的な絵算がうまく働かない例になっているようです。しょうがないので、別な手段 -- 圏論的行列計算を使うことにします、たぶん。
圏論的行列計算は、計算手順は普通の行列計算とまったく同じですが、計算の意味論をモノイド圏のなかに取ります。ワイヤリングが複雑化しちゃったときは、直接絵算より行列計算したほうがうまく行くときもあります。
[追記]二転三転ですが、やっぱり行列計算じゃなくて、直接的な絵算を使おうかと。行列計算は、発見的手法としても雑談ネタとしても面白いのですが、今回のケースでは、実用上受け入れがたい制限を付けるか、あるいは非決定性を導入して新しい圏を構成するとか、セットアップに手間がかかるんです。時間的に無理な感じ。
レイアウトに注意して描けば、直接絵算でもまーなんとかなるかな、っと。さっき絵を描いていたら、最後の最後になって、右と左を逆にすれば良かったことに気が付きました。ウゲーー、もうウンザリ。描き直す気力がないので、余分なスワップ(左右交換)が入るけど、これでもういいことにします。[/追記]
実務上の要請と帰結
「モニャドセミナー4の予定:トランザクション計算のフレームワークとか」の冒頭で言ったとおり、今回は、「アブストラクト・ナンセンスが実務的な問題解決にどう利用できるか」ってことをデモンストレートしたいのです。その実務的観点をまとめると:
- プラッガブル・コンポネントとフレームワークにより、ある種のトランザクション計算(エコ計算と呼ぶのが適切?)のメカニズムを作りたい。
- コンポネント作成者の負担をできるだけ少なくしたい。特に、退屈なルーチンコードを書くようなことは強制しない。
- フレームワークの実装もできるだけ単純にしたい。既存の知識やコードで済むならそれで済ませたい。
- 実行される計算が、型安全であることを保証したい -- 型エラーが起きないことは実行をせずにチェックしたい。
- 一見矛盾するような要求を調停するために、コンポネント群の組み立てと実行に先立ち、静的または動的にラッピングをする。ラップされたコンポネント群をフレームワークの実行環境上で走らせる。