2006-12-14 騏驎も老いては駑馬に如かず [長年日記]
λ. Domain Theoretic Models Of Polymorphism by Thierry Coquand and Carl A. Gunter
読みかけ。
cocontinuous な functor F: C→DEP から、Grothendieck construction で圏 ΣF と射影 p:ΣF→C を定義する。CがdomainならΣFもdomainになっている。pのcoconitnuousなセクション C→ΣF とその間の自然変換からなる圏を ΠF とする。Cがdomainなら ΠF もdomainになっている。
CをDEP自身とする。このときΣFは半順序集合にならない。ΠFは半順序「集合」にはならずクラスになるが、圏同値なdomainが存在する。このΠを使って多相型を扱う。
このモデルはuniformに振舞わないような多相的な要素を含む。 admissibleな関係に限定した場合のparametricityは……やっぱり成り立たないのかな?*1
*1 もし成り立つのであれば Shortcut fusion is correct はインパクトを持たない気がするし
λ. 凄い漢字
<URL:http://www.rubyist.net/~matz/20061204.html#p02> にツッコミをいれようとしたら、spamフィルタに弾かれたみたいなので、こっちに。その「うしのあゆみがおそい」はU+3E2A(「㸪」)として既に含まれているような。