Declarative Continuations and Categorical Duality by Andrzej Filinski - bonotakeの日記

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

[hengsu]

『値と継続が双対 (dual)の関係にある』関数空間の双対の双対が元の関数空間だから、