ExistentialQuantificationを使用して と同等の機能を実現できるという主張をいくつかの場所で読みましたRankNTypes。誰かがこれが可能である、または不可能である理由の例を提供できますか?
2 に答える
11
通常、Haskellのすべての型変数は、型の最も外側のスコープで暗黙的に全称記号化されます。 RankNTypes全称記号forallをネストされたように見せることができます。たとえば、型forall a b. (a -> a) -> b -> bはとは大きく異なり forall b. (forall a. a -> a) -> b -> bます。
関数の矢印の左側にある型が論理的に「否定」されているという意味があります。これ(->)は、論理的な意味とほぼ同じ意味です。論理的には、普遍的および存在記号はド・モルガンの二重性によって関連付けられます：（∃x.p（x））は¬（∀x.¬P（x））と同等です。 P（x）」は、「すべてのxについて、P（x）が偽であるとは限らない」に対応します。
したがって、関数矢印の左側にあるフォラルは「否定」され、実存的なもののように動作します。全体を別の関数矢印の左側に置くと、それは二重否定になり、いくつかの厄介な詳細を法として、再び全称記号として動作します。
同じ否定の考え方が値にも当てはまるので、必要な型exists x. xをエンコードするには、次のようにします。
forall x.反変（否定）位置- 共変（正）の位置
xにあるそのタイプの値。
値は数量詞の範囲内にある必要があるため、基本的にCPS変換である二重否定のみを選択します。それ以外の制限を回避するために、関数の矢印の右側にあるタイプを全称記号で定量化します。したがってexists x. x、に変換されforall r. (forall x. x -> r) -> rます。ここでの型と数量詞の配置を上記の要件と比較して、要件を満たしていることを確認します。
より操作上の用語では、これは、上記のタイプの関数が与えられた場合、全称記号の引数タイプの関数を与えるため、その関数をx好きなタイプに適用でき、他に取得する方法がないことを意味します。タイプの値は、その関数を何かrに適用することがわかっています。したがって、あるタイプを参照しますが、それが何であるかはわかりません。これが基本的に存在記号の本質です。x
より実用的な日常の用語では、関数型の「反対側」から見た場合、全称記号型変数は存在すると見なすことができます。型推論の一部として実行される統合は数量詞スコープを超えるため、GHCが外部スコープの型変数をネストされたスコープの数量化された型と統合しなければならない状況になることがあります。これにより、コンパイラエラーが発生します。型やスコーレムのエスケープなどについては、後者（私は推測します）はスコーレム標準形に関連しています。
これが存在を使用するデータ型に関連する方法は、次のような型を宣言できることです。
data Exists = forall a. Exists a
これは実存型を表します。「実存型」を取得するには、パターンマッチングによってそれをアンラップする必要があります。
unexist :: Exists -> r
unexist (Exists x) = foo x
ただしfoo、この定義でのタイプを考慮forall a. a -> rすると、上記のCPSスタイルのエンコーディングと同等ののようなものになります。CPS変換とデータ型のチャーチエンコーディングの間には密接な関係があるため、CPSフォームはパターンマッチの改良版と見なすこともできます。
最後に、物事をロジックに関連付けます。これは、「存在記号」という用語の由来であるためです。矢印の左側を否定として考え、forall r. ...CPSの残骸を無視するために目を細めて考える場合、これらの存在型のエンコーディングに注意してください。出発点であったDeMorganの二重化された形式¬（∀x.¬P（x））とまったく同じものです。したがって、これらはすべて、同じ概念を見る異なる方法にすぎません。
于 2013-01-24T00:29:18.303 に答える
3
于 2013-01-24T02:31:33.607 に答える