当該タイトルの論文は http://dx.doi.org/10.1145/1411203.1411226 論文では Coqで書いてあるが、同じことが Haskell (+GADT) でもできるようで、Haskell-cafe に投稿されていた： http://www.mail-archive.com/haskell-cafe@haskell.org/msg48913.html HOAS…

と、自分でも何を言ってるのか分からねーですが、タイトルに継続と書けばとアクセス数とブクマが増えるのでそう書く(←最低)。あながち遠くはないはずだけどOCamlでHaskellのforall を使うような存在型を直接書く事はできないらしい。 そこで #002 存在型 - K…