存在型を全称限量子と代数的データ型でエンコードする

Coq Haskell

HaskellのGHC言語拡張に含まれる存在型は、existential quantifierを使わずにuniversal quantifierと代数的データ型を組み合わせて表現されます。以前からどうしてこんなことができるのかと思っていたのでそのカラクリを調べてみました。

GHC言語拡張では存在型を次のように定義できます。

{-# LANGUAGE ExistentialQuantifications #-}
data Q = forall x. P x

このように型引数を取らないデータ型のデータ構成子に、全称量化された変数を持つような型を定義します。この定義は直接existential quantifierを使えば次のように表現できるものです。

-- 疑似Haskell。GHCではコンパイルできない。EHCならできるかも。
data Q = P (exists x. x)

データ構成子の中と外でquantifierがひっくり返るイメージです。

これはどうやら述語論理の

という関係に基づいているようです。見比べてみると確かにそっくりです。

天下り的にこの関係を使っても良いのですが、せっかくなのでつたないながら自力でCoqで証明してみました。

ソート（TypeやProp）の使い分けがよくわからないとか、左向きと右向きのどちらも証明した後でイコールを証明するやり方がわからないとか、いろいろわからないまま使っているので、Coq使いの皆さま是非アドバイスをください。

参考