「例外付き計算とグロタンディーク構成」で述べた話の双対をとると、環境付き計算になります。
「環境」という言葉はいろいろな意味で用いられますが、ここでの環境はOSの環境変数に類似した概念で、プログラムから参照可能な大域変数といった意味です。環境は次の条件を満たすとします。
- 読み取りはできるが書き換えはできない。
- 時間的に値が変動しない。
- 複数の計算単位から参照できる。
値が変わらないので変数というよりは定数です。大域的な設定(configuration)情報と考えればいいでしょう。
例外と環境は次のような対応により双対となります。
例外 | 環境 |
---|---|
出力 | 入力 |
直和 + | 直積 × |
モノイド | 余モノイド |
余対角 ∇ | 対角 Δ |
始対象 0 | 終対象 1 |
例外型 | 環境型 |
例外変換 | 環境変換 |
余インデックス付き圏 | インデックス付き圏 |
純粋計算の圏をCとして、環境型と環境変換の圏をGとすると、CとGからインデックス付き圏が作れて、グロタンディーク構成ができます。平坦化された圏の射は環境付き計算とみなせます。例外付き計算のときと全く同じです。
例外と環境はほんとにキッチリと双対なので、別々に扱うのは得策ではありません。一緒に扱うべきでしょう。例外&環境付き計算は、絵算を使ってもグロタンディーク構成を使っても定式化できます。型システムとしてはタプル型とユニオン型の導入、論理ならばANDとORの計算に対応します。
純粋計算に例外と環境を加えた計算は、計算モデルとしては比較的単純な部類でしょうが、それでも細部まで詰めるのはけっこう面倒です。この計算モデルを調べておく必要性もあるし適当な素材だから、まーやってみるか、とは思っていますがね。