まず、コンピュータプログラムの型が直観主義論理の公式に対応していると述べている「カリーハワード対応」を見てみましょう。直観主義論理は、学校で学んだ「通常の」論理と同じですが、排中律または二重否定の除去の法則がありません。
論理の法則
あなたはド・モルガンの法則を順調に進んでいますが、最初にそれらを使用していくつかの新しい法則を導き出します。ド・モルガンの法則の関連するバージョンは次のとおりです。
- ∀x。P（x）=¬∃x。¬p（x）
- ∃x。P（x）=¬∀x。¬p（x）
（∀x。P⇒Q（x））=P⇒（∀x。Q（x））を導出できます。
- （∀x。P⇒Q（x））
- （∀x.¬P∨Q（x））
- ¬P∨（∀x。Q（x））
- P⇒（∀x.Q）
そして（∀x。Q（x）⇒P）=（∃x。Q（x））⇒P（これは以下で使用されます）：
- （∀x。Q（x）⇒P）
- （∀x.¬Q（x）∨P）
- （¬¬∀x.¬Q（x））∨P
- （¬∃x。Q（x））∨P
- （∃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
existsHaskellに構文がないことを除いて。
非直観主義論理では、次のタイプから次のことを導き出すことができますunCon。
unCon :: ∃ T -> t -- invalid!
これが無効である理由は、そのような変換が直観主義論理で許可されていないためです。したがってunCon、キーワードなしで型を記述するexistsことは不可能であり、型署名を冠頭標準形にすることは不可能です。このような条件で型チェッカーが終了することを保証するのは難しいので、Haskellは任意の存在記号をサポートしていません。
ソース
「型推論による一流のポリモーフィズム」、Mark P. Jones、プログラミング言語の原理に関する第24回ACM SIGPLAN-SIGACTシンポジウムの議事録（web）