双対性と随伴関手
Menu Menu関数型言語の計算は項の変換に過ぎないが、入出力や失敗あるいは並行実行のような概念が計算には付属している。これをメタケイ酸という。
例えば、
puts("hello wolrd!\n");
は、外部の世界に文字列を表示するという機能がある。
これは隠れた大域変数があって、それを操作している考えることもできる。しかし、Haskellのようなpureな関数型言語では、
f ( g x ) ( h y )という呼び出しがあった時に、f g h のどれが先に実行されるかはわからない。単なる大域変数では結果が実行系の実装に依存してしまう。
これは、f g h という関数と f' g' h' というメタ計算を含む関数の実行が対応していてほしいという要求になる。
計算⇔メタ計算
という。関数型言語の世界は集合を対象とする圏Setsだった。なので、
Sets⇔メタ計算の圏
という風になって欲しい。メタ計算も結局は関数型言語でsimulationできると考えると、メタ計算の圏も結局はSetsになる。ここではK と書こう。
圏と圏の対応は関手(Functor)で行われるので、
F : Sets → K
U : K → Sets
という二つの関手があることになる。
Hom Sets a bはSetsという圏の対象aから対象bへの射の集合であるとする。これは集合だから型である。
f : Hom Sets a b は、 f : a → bのこと。K の方は単なる関数ではなくてメタ計算を含む関数ということになる。
単純にHom Sets a b がHom K a b に対応するということはできない。
FMap F : Hom Sets a b → Hom K Fa Fb
FMap U : Hom K a b → Hom Sets Ua Ub
はある。Sets ⇔ K から FU=1, UF=1 を要求すると、K はSets と同じ圏になってしまう。計算とメタ計算の対応はUF=1ではあり得ない。
FU,UFが1でないということは、UまたはFが全射ではないことを含んでいる。つまりUbはObj Setsの部分集合である。
例えば、非決定性のある計算を考えよう。ある関数は複数の可能な値を返す。それをリストを使って表そう。
g f
a -------> b --------> c
[a] ------> [b] ------> [c]
g' f'
ここではKは[a]を対象とするSetsの部分圏Listである。
F : Sets -> List
F = record {
FObj = λ x → List x
FMap f [] = []
; FMap f (h :: t) = (f h) :: FMap f t
}
は list のFunctor である。U はいろんな可能性があるが、例えば、
U : List -> Sets
U = record {
FObj = λ (x : List a) → a
; FMap f x = head ( f ( x :: [] ) )
}
ここで対応しているのは、
その代わり、
Hom K Fa b ⇔ Hom Sets a Ub
という対応がある。このaとbにそれぞれ関数hを作用させると、
Hom K Fa b ⇔ Hom Sets a Ub
| |
|Ff |f
↓ ↓
Hom K F(f a) b ⇔ Hom Sets (f a) Ub
Hom K Fa b ⇔ Hom Sets a Ub
| |
|f |Uf
↓ ↓
Hom K Fa (f b) ⇔ Hom Sets a U(f b)
ということになる。この可換図が成立していて欲しい。
