PolyPCF vs Haskell

ところで、PolyPCFが、Haskellを表現する適切なモデルなのかというと、Haskellには、seqという関数が存在して(seqってGHC固有の関数じゃないよね？たぶん)、seqが絡むと、リストに限ってもshortcut fusionが成立しなくなる(参考)ので、PolyPCFとHaskellは違うもの。逆に言うと、特定の言語で、融合変換を無条件に行っていいかどうかというのは、そんなに自明でもなくて、きちんとsemanticsを定義した上で吟味されるべき事項だとか、そんなこんな

PolyPCFの定義について。PolyPCFは名前からしてPCFという体系にPolymorphismを付け加えたもの。オリジナルのPCFは、(確か)自然数やboolをプリミティブに含んでいるけど、PolyPCFでは、Church encodingを利用するとかして、自然に自然数型、ブール型、リスト型を定義できて、適切な設定の下で、プリミティブとして付け加えた自然数型、ブール型、リスト型と同型になるんでないかな、おそらく。確かめてはないけど(リスト型の場合については、Pittsが証明済)。なお、以下型Aと型Bが同型といったら、a::A->Bとb::B->Aで、a (b x) = x , b (a y) = yを満たすものが存在することをいうことにする。型の直積や直和についても、丁度、System Fでそうであるように、PolyPCFでも定式化できて、敢えてプリミティブとして付け加える必要もないんじゃないかと予想する。あと、existential typeについても、同様の事実がPittsの論文に書かれていた。PolyPCFのちょっと面白い性質として、型forall x.xを持つclosed termは、System Fでは存在しなかったけど、PolyPCFだと、fix idで表現できる

で、seq以外で、PolyPCFになくて、Haskell(そのものより、GHC Coreとかの方がよいが)にあるもの。ぱっと思いついたのは

・型クラス。forall a.(Eq a)=>a->a->Boolみたいな型は、PolyPCFでは無理
・モナドから値を取り出す"illegal"な関数群(fromJustとかunsafePerformIO)やIORef
・nested datatypesは、PolyPCFではモデル化できなくね？

あたり。微妙に、どこまでがhaskellの仕様で定められてるものなのか分からんけど、しらべんのがめんどい。型クラスはよくわからんので放置。IORefとかはどうなんでしょうねぇ。真面目に考えると、semanticsに乗せにくそうなんで、深く考えない方向で。てことで、面白そうなのは3番目のnested datatypesなわけですが、いまいちコレが何に使えるのか実感がわかないので、食指が動かないのだった。ていうか、本当にモデル化できないのかとか、怪しいけど、多分できないよね。