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

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

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

参照用 記事

作用と例外を含む計算の一般化クライスリ圏

交替律と分合律」にて:

ストレージIOを含む例外付き計算の一般化クライスリ圏が、イミュータブルな場合の自然な拡張として作れるはずです。作れたらいいな … 。

たぶん出来たような気がする。一番簡単な場合のクライスリ射は次のような感じ。

A, B, E は集合圏Setの対象で、M, Nはモノイドの圏(モノイド圏ではない)Monの対象。ほんとは、SetMonを分離して扱わないとマズイですが、面倒なのでMonSetの部分圏のような言い方をします。

E, M, N は一時的に固定します。E, M, N をインデックス圏のベースとして動かせば、任意の E, M, N を扱えますが、とりあえずは局所的な話(つまり、ひとつのファイバーだけを見る)。

f: A → (M:×B) +: E と書いたら、「:×」は直積で「+:」は直和ですが、「:×」の左は作用を表現するモノイド、「+:」の右側は例外の型だと解釈します。ですが、こんな記号は覚えにくいので、自然言語風の次の記法も使います。


f requires A as input
(returns B as output
and
posts M as effect
)
or
throws E as exception

上の図のhは例外ハンドラーで、例外時の処理として型Nのデータを作用キューにポストしてから例外を再スローするとします。この例外ハンドラーhはプログラマが書くのではなくて勝手に付加されるものです。fとhをまとめた処理をgとすると、その仕様(プロファイル)は次のように書けます。


g requires A as input
(returns B as output
and
posts M as effect
)
or
(throws E as exception
and
posts N as effect
)

さらに、交替律を使って and と or を入れ替えると次のようになります。


k requires A as input
(returns B as output
or
throws E as exception
)
and
posts (M or N) as effect

kは、fから一意的に決まります。例外のあるなしに関わらず、作用は必ずキューにポストされます。Mが正常時の作用、Nが異常時(例外が起きたとき)の作用です。M or N はモノイドの直和(自由積です)を意味します。Nが単位だけの自明なモノイドなら、M or N はM と同じです。このときは、例外なら何もしないこと(モノイド単位の作用)になります。

以上のようにして作ったkがクライスリ射です。つまり、SetMonが混じったような圏のなかで、k : A → (M + N)×(B +:E) があると、それはクライス圏Kの射 f: A→B in K を定義します。クライスリ射の結合は少し面倒ですが、普通にやれば定義できます。

今の例は、作用モナドと例外モナドを交替律で組み合わせましたが、実際はとある双モナド*1と例外モナドと組み合わせるのでもう少し複雑になります。が、ややこしくなる以外の困難はないように思われます(交替律の厳密な定式化はけっこう手間がかかりそうですが)。

[追記]

M or N はモノイドの直和(自由積です)を意味します。

直和だというのはオカシイかもしれない。だけど、

Nが単位だけの自明なモノイドなら、M or N はM と同じです。このときは、例外なら何もしないこと(モノイド単位の作用)になります。

この結果は変わらないので、当面の目的には影響しないです。

もともと、「交替律」という言葉は便宜的で、表層的な形が似ているのでそう呼んでましたが、内容的にはだいぶ違うのかもしれません。

(交替律の厳密な定式化はけっこう手間がかかりそうですが)。

試行錯誤の結果として表層的な形はだいたいわかるんですが、メカニズムが完全には分かってないです。

[/追記]
[さらに追記]

表層的な形はだいたいわかるんですが、メカニズムが完全には分かってないです。

実装するには問題ない、うまくいきそうだ、という点では結果オーライだけど、どこかで何かがズレている

疑わしいのは、例外処理がうまくいく事情が、交替律の類似とは別な事情かもしれないことですね。

[/さらに追記]

*1:モナドよりもさらに複雑かも。