値と継続が双対 (dual)の関係にあることを初めて知る。
以下、自分の思考をだらだらと書き留めたチラシの裏。なんのまとまりもありません。あと、元論文の解説ではなくて、読みながら考えたことを書いてるので注意。実は違う話をしてる可能性大。
それから、タイトルの論文の著者がどういう圏を構成しているのか、イマイチ不明なところがあり*1。でもλ計算に継続を入れた世界を考えてるので、CCCであることは仮定していいんだろう。
f:X → Y
が「型Xの値を引数に取り、型Yの値を戻り値に持つ関数」なのは良い。ここで、f, X, Yのそれぞれの双対 ~f, ~X, ~Yを考えてみる。（記法は、この後に出てくる表現も含めて、元論文と全然違います。私が適当に考えました）
~Xを「型Xの値を要求（request）する継続」だと解釈するならば、
~f:~Y → ~X
（矢印の向きが逆になっているのに注意）は、「型Yの値を要求する継続」から「型Xの値を要求する継続」への「関数」であって、~Yは~fを通じて型Xの値を要求することになる。…という解釈であってるのだろか。
じゃあ、継続 ~X って結局何よ？
ここで仮に、型Xの値をとって何か（仮に型Aとしておく）を返す関数のようなものなのだと思い込んでみる。すなわち、~X ＝ AX（冪対象、XからAへの関数空間をあらわすもの）とおく*2。
で、Aが何にあたるのか、をずーっと考えてたんだけど、カリーハワードの何とやらを思い出すと、結局これは⊥ってことか。つまり、X × ~X を eval すると⊥が返る（というか、返って欲しい）。そうすると、論理の世界で
X ∧ ¬X → false
を対応させられる。（"~"って記号、最初は適当に選んでみたんだけど、偶然にもかなり上手くハマってしまった。）
結局のところ、自分の知識を違った方面から再整理することになった。その後、継続に詳しいid:ku-ma-meさんとかと話していろいろ考えた自分なりの超アバウトな結論としては：
継続っつーのは値を入れる「器」みたいなもの。あるいは、「値」を吸収すると消滅してしまう何か。「値」そのもの（例えば、式がどう評価されるか）には関わらない。あくまで、制御の流れだけに寄与する。
それが値の双対概念と言うことであり、戻り値の型が⊥ということにつながるんだと思われる。
元の論文の話に戻りますが、ずいぶん読みやすいD論だなぁ、と思ったら修論でした。categorical、とあるけど、圏論的な考察はそれほど深くない。あと、個人的に納得いかなかったりするところも。でも上の洞察は面白い。
