存在types的理论基础是什么？
Haskell维基解释如何使用存在types做了很好的工作，但是我不太理解它背后的理论。
考虑这个存在types的例子：
data S = forall a. Show a => S a -- (1) 为我们可以转换为String东西定义一个types包装器。 维基提到，我们真正想要定义的是类似的
data S = S (exists a. Show a => a) -- (2)
即一个真正的“存在”types – 松散的我认为这是说“数据构造函数S采取任何types的Show实例存在和包装它”。 实际上，你可以写一个GADT，如下所示：
data S where -- (3) S :: Show a => a -> S
我没有尝试编译，但似乎它应该工作。 对我来说，GADT显然等同于我们想写的代码（2）。
然而，我完全不明白为什么（1）等同于（2）。 为什么把数据构造函数移到外面会把所有的东西变成exists ？
我能想到的最接近的是德摩根的逻辑规律 ，交换否定顺序和量词将存在量词转换为通用量词，反之亦然：
¬(∀x. px) ⇔ ∃x. ¬(px)
但数据构造者似乎是否定运算符的完全不同的野兽。
存在的定义存在types背后的理论是什么，而不是不存在的exists ？
首先，看一下“咖喱霍华德通信”，它表示计算机程序中的types与直觉逻辑中的公式相对应。 直觉主义逻辑就像你在学校学到的“正规”逻辑，但没有被排除的中间或双重否定消除的规律：
-
不是一个公理：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））：
- （∀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
请注意，这些规律也在直觉逻辑中。 我们得出的两个法则在下面的文章中被引用。
简单的types
最简单的types很容易处理。 例如：
data T = Con Int | Nil
构造函数和访问器具有以下types签名：
Con :: Int -> T Nil :: T unCon :: T -> Int unCon (Con x) = x
types构造函数
现在我们来处理types构造函数。 采取以下数据定义：
data T a = Con a | Nil
这创build了两个构造函数，
Con :: a -> T a Nil :: T a
当然，在Haskell中，typesvariables是隐含地普遍量化的，所以这些实际上是：
Con :: ∀a. a -> T a Nil :: ∀a. T a
访问器同样简单：
unCon :: ∀a. T a -> a unCon (Con x) = x
量化的types
让我们将存在量词∃添加到我们的原始types（第一个，没有types构造函数）。 而不是将其引入类似于逻辑的types定义中，而是将其引入构造函数/访问器定义中，这看起来像逻辑。 稍后我们将修复数据定义以匹配。
现在我们将使用∃x. t代替Int ∃x. t ∃x. t 。 这里， t是某种types的expression。
Con :: (∃x. t) -> T unCon :: T -> (∃x. t)
根据逻辑规则（上面的第二条规则），我们可以将Con的types重写为：
Con :: ∀x. t -> T
当我们把存在量词移到外部时（prenexforms），它变成了一个通用的量词。
所以以下是理论上等价的：
data T = Con (exists x. t) | Nil data T = forall x. Con t | Nil
除了在Haskell中没有exists语法。
在非直觉逻辑中，允许从unContypes中推导出以下unCon ：
unCon :: ∃ T -> t -- invalid!
这是无效的原因是因为直觉逻辑不允许这样的转换。 所以如果没有exists关键字，就不可能为unCon写入types，并且不可能将types签名置于前置forms。 很难让types检查器保证在这种情况下终止，这就是为什么Haskell不支持任意存在量词的原因。
来源
“types推理的一类多态性”，Mark P. Jones，第二十四届ACM SIGPLAN-SIGACT程序devise语言原理（ networking ）研讨会论文集，
Plotkin和Mitchell在他们着名的论文中build立了一种存在types的语义，使得编程语言中的抽象types与逻辑中的存在types之间存在联系，
米切尔，约翰·C。 Plotkin，Gordon D. 抽象types有存在型 ，编程语言和系统ACM交易，卷。 1988年7月第3号，第470-502页
在高层，
抽象数据types声明以类似于Ada，Alphard，CLU和ML的编程语言出现。 这种声明forms将一系列标识符绑定到一个具有相关操作的types上，这个复合“值”我们称之为数据代数。 我们使用一个二阶types的lambda演算SOL来显示数据代数是如何被赋予types，作为parameter passing的，并作为函数调用的结果返回。 在这个过程中，我们讨论抽象数据types声明的语义，并回顾types化编程语言和构造逻辑之间的联系。
这是在你链接的haskell wiki文章中说明的。 我会借用一些代码和评论，并试图解释。
data T = forall a. MkT a
这里有一个types为T的types构造函数MkT :: forall a. a -> T MkT :: forall a. a -> T ，对吗？ MkT （大体上）是一个函数，所以对于每种可能的typesa ，函数MkT都有typesa -> T 所以，我们同意通过使用这个构造函数，我们可以build立像[MkT 1, MkT 'c', MkT "hello"] ，它们都是Ttypes的。
foo (MkT x) = ... -- what is the type of x?
但是当你试图提取（例如通过模式匹配）包含在T的值时会发生什么？ 它的types注解只是说T ，没有任何引用实际包含的值的types。 我们只能认同这样一个事实，不pipe它是什么样的，它只有一个（也是唯一的一个）types的; 我们如何在Haskell中说明这一点？
x :: exists a. a
这只是说，存在一个x所属的types。 在这一点上，应该清楚的是，通过从MkT的定义中除去所有的forall a ，并明确指定包装值的types（即exists a. a MkT ），我们能够得到相同的结果。
data T = MkT (exists a. a)
底线是相同的，如果你像在你的例子中那样在实现的types类中添加条件。
