値と継続が双対 (dual)の関係にあることを初めて知る。 以下、自分の思考をだらだらと書き留めたチラシの裏。なんのまとまりもありません。あと、元論文の解説ではなくて、読みながら考えたことを書いてるので注意。実は違う話をしてる可能性大。 それから、タイトルの論文の著者がどういう圏を構成しているのか、イマイチ不明なところがあり*1。でもλ計算に継続を入れた世界を考えてるので、CCCであることは仮定していいんだろう。 f:X → Y が「型Xの値を引数に取り、型Yの値を戻り値に持つ関数」なのは良い。ここで、f, X, Yのそれぞれの双対 ~f, ~X, ~Yを考えてみる。(記法は、この後に出てくる表現も含めて、元論文と全然違います。私が適当に考えました) ~Xを「型Xの値を要求(request)する継続」だと解釈するならば、 ~f:~Y → ~X (矢印の向きが逆になっているのに注意)は、「型