☰

存在型の理論的根拠は何ですか? 質問する

tag-icon • tag-icon haskell types type-systems existential-type quantifiers
存在型の理論的根拠は何ですか? 質問する

のハスケルウィキ存在型の使い方についてはうまく説明されていますが、その背後にある理論はよくわかりません。

存在型のこの例を考えてみましょう。

data S = forall a. Show a => S a      -- (1)

に変換できるものの型ラッパーを定義するString。ウィキによれば、本当に定義したいのは次のような型です

data S = S (exists a. Show a => a)    -- (2)

つまり、真の「存在型」です。大まかに言うと、データコンストラクタはインスタンスSが生成される任意の型を受け取ります。Show存在するそしてそれをラップします」。実際、GADT は次のように記述できるでしょう。

data S where                          -- (3)
    S :: Show a => a -> S

コンパイルは試していませんが、動作するはずです。私にとって、GADT は明らかに、記述したいコード (2) と同等です。

しかし、(1) が (2) と同等である理由がまったくわかりません。データ コンストラクターを外側に移動すると、 がforallに変わるのはなぜですかexists?

私が思いつく最も近いものはド・モルガンの法則論理学では、否定と量指定子の順序を入れ替えると、存在量指定子が全称量指定子に変わり、その逆も同様です。

¬(∀x. px) ⇔ ∃x. ¬(px)

しかし、データ コンストラクターは否定演算子とはまったく異なるもののようです。

forall存在しない の代わりにを使用して存在型を定義できる能力の背後にある理論は何ですかexists?

ベストアンサー1

まず、「カリー・ハワード対応」を見てみましょう。これは、コンピュータ プログラム内の型が直観主義論理の式に対応することを示しています。直観主義論理は、学校で習った「通常の」論理とまったく同じですが、排中律や二重否定消去法がありません。

  • 公理ではありません: P ≡ ¬¬P (ただし P ⇒ ¬¬P は問題ありません)

  • 公理ではない: P ∨ ¬P

論理の法則

ド・モルガンの法則については正しい方向に進んでいますが、まずはそれを使って新しい法則を導き出しましょう。ド・モルガンの法則の関連バージョンは次のとおりです。

  • ∀x. P(x) = ¬∃x. ¬P(x)
  • ∃x. P(x) = ¬∀x. ¬P(x)

(∀x. P ⇒ Q(x)) = P ⇒ (∀x. Q(x)) を導出できます。

  1. (∀x.P ⇒ Q(x))
  2. (∀x. ¬P ∨ Q(x))
  3. ¬P ∨ (∀x. Q(x))
  4. P ⇒ (∀x. Q(x))

そして、(∀x. Q(x) ⇒ P) = (∃x. Q(x)) ⇒ P (これは以下で使用されます):

  1. (∀x. Q(x) ⇒ P)
  2. (∀x. ¬Q(x) ∨ P)
  3. (¬¬∀x. ¬Q(x)) ∨ P
  4. (¬∃x. Q(x)) ∨ P
  5. (∃x. Q(x)) ⇒ P

これらの法則は直観主義論理にも当てはまることに注意してください。私たちが導き出した 2 つの法則は、以下の論文で引用されています。

単純型

最も単純なタイプは簡単に操作できます。例:

data T = Con Int | Nil

コンストラクターとアクセサーには次の型シグネチャがあります。

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

型コンストラクタ

それでは、型コンストラクタについて考えてみましょう。次のデータ定義を見てみましょう。

data T a = Con a | Nil

これにより、2つのコンストラクタが作成されます。

Con :: a -> T a
Nil :: T a

もちろん、Haskell では型変数は暗黙的に全称量化されるため、実際には次のようになります。

Con :: ∀a. a -> T a
Nil :: ∀a. T a

アクセサも同様に簡単です:

unCon :: ∀a. T a -> a
unCon (Con x) = x

定量化されたタイプ

存在量指定子 ∃ を元の型 (型コンストラクターのない最初の型) に追加してみましょう。ロジックのように見えない型定義で導入するのではなく、ロジックのように見えるコンストラクター / アクセサー定義で導入します。後でデータ定義を修正して一致させます。

の代わりにInt、 を使用します∃x. t。ここで、tは何らかの型式です。

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

論理のルール (上記の 2 番目のルール) に基づいて、 の型をCon次のように書き換えることができます。

Con :: ∀x. t -> T

存在量指定子を外側（冠頭形式）に移動すると、全称量指定子に変わりました。

したがって、理論的には次のものは同等です。

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

existsただし、 Haskell には の構文はありません。

非直観主義論理では、 の型から次のものを導出することが許容されますunCon。

unCon :: ∃ T -> t -- invalid!

これが無効である理由は、このような変換は直観主義論理では許可されていないためです。したがって、キーワードunConなしで型を記述することは不可能でexistsあり、型シグネチャを冠頭形式にすることは不可能です。このような状況で終了することを保証する型チェッカーを作成するのは難しいため、Haskell は任意の存在量指定子をサポートしていません。

出典

「型推論による第一級ポリモーフィズム」、マーク・P・ジョーンズ、プログラミング言語の原理に関する第24回ACM SIGPLAN-SIGACTシンポジウム議事録（ウェブ）

おすすめ記事