双対性と環境付き計算

「例外付き計算とグロタンディーク構成」で述べた話の双対をとると、環境付き計算になります。

「環境」という言葉はいろいろな意味で用いられますが、ここでの環境はOSの環境変数に類似した概念で、プログラムから参照可能な大域変数といった意味です。環境は次の条件を満たすとします。

1. 読み取りはできるが書き換えはできない。
2. 時間的に値が変動しない。
3. 複数の計算単位から参照できる。

値が変わらないので変数というよりは定数です。大域的な設定（configuration）情報と考えればいいでしょう。

例外と環境は次のような対応により双対となります。

例外	環境
出力	入力
直和 +	直積 ×
モノイド	余モノイド
余対角 ∇	対角 Δ
始対象 0	終対象 1
例外型	環境型
例外変換	環境変換
余インデックス付き圏	インデックス付き圏

純粋計算の圏をCとして、環境型と環境変換の圏をGとすると、CとGからインデックス付き圏が作れて、グロタンディーク構成ができます。平坦化された圏の射は環境付き計算とみなせます。例外付き計算のときと全く同じです。

例外と環境はほんとにキッチリと双対なので、別々に扱うのは得策ではありません。一緒に扱うべきでしょう。例外＆環境付き計算は、絵算を使ってもグロタンディーク構成を使っても定式化できます。型システムとしてはタプル型とユニオン型の導入、論理ならばANDとORの計算に対応します。

純粋計算に例外と環境を加えた計算は、計算モデルとしては比較的単純な部類でしょうが、それでも細部まで詰めるのはけっこう面倒です。この計算モデルを調べておく必要性もあるし適当な素材だから、まーやってみるか、とは思っていますがね。