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

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

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

参照用 記事

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

予定している筋書きは「モニャドセミナー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は関手である。

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

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

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

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

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

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

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

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

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

実務上の要請と帰結

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

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

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

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