パラメトリシティとseq

ググっていたら見つけたエントリ「GHCは気色悪い」について．

これは GHC が気色悪いのではなくて，seq が気色悪いのではないかと． seq があると，パラメトリシティを維持するためには論理関係 R が admissibile（連続かつ正格）なだけでは不十分で bottom-reflecting（a R b に対し a≠⊥ ⇔ b≠⊥ ）が必要になる． ここでは， その条件を少し緩めて R が全域（a R b に対し a≠⊥ ⇒ b≠⊥）とすることで， free theorem の不等式版などを導出できることを示している． 個人的には，Pitts的な操作的（かつ構文的）アプローチにも興味があるが， TT-closed は admissibility より強すぎるので seq と絡めるには別の新しいアイデアが必要かも．

[追記] 「激しく被られた！」といっても時間的にはこちらの方が後だったり．

[追記2] syntacticの訳は「構文的」の方がよいと思ったので修正しました．

[追記3] この日記で漸くはてなダイアリー市民になったようです．

[追記4] こちらの追記の補足のため，Abadiの論文への参照を追加．