首先，看一下“Curry Howard 对应”，它指出计算机程序中的类型对应于直觉逻辑中的公式。直觉逻辑就像你在学校学到的“常规”逻辑，但没有排中律或双重否定消除法：
逻辑法则
你在德摩根定律的正确轨道上，但首先我们将使用它们来推导出一些新的定律。德摩根定律的相关版本是：
- ∀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
请注意，这些定律也适用于直觉逻辑。我们得出的两个定律在下面的论文中被引用。
简单类型
最简单的类型很容易使用。例如：
data T = Con Int | Nil
构造函数和访问器具有以下类型签名：
Con :: Int -> T
Nil :: T
unCon :: T -> Int
unCon (Con x) = x
类型构造函数
现在让我们处理类型构造函数。采用以下数据定义：
data T a = Con a | Nil
这会创建两个构造函数，
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)
根据逻辑规则（上面的第二条规则），我们可以将类型重写Con为：
Con :: ∀x. t -> T
当我们把存在量词移到外面（前缀形式）时，它变成了一个全称量词。
所以以下理论上是等价的：
data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil
exists除了Haskell中没有 for 的语法。
在非直觉逻辑中，允许从 的类型推导出以下内容unCon：
unCon :: ∃ T -> t -- invalid!
这是无效的原因是直觉逻辑中不允许这样的转换。所以unCon没有exists关键字就不可能写出for的类型，也不可能把类型签名放在prenex形式中。很难让类型检查器保证在这种情况下终止，这就是 Haskell 不支持任意存在量词的原因。
来源
“First-class Polymorphism with Type Inference”，Mark P. Jones，第 24 届 ACM SIGPLAN-SIGACT 编程语言原理研讨会论文集（网络）