存在类型的理论基础是什么？
Haskell Wiki在解释如何使用存在类型方面做得很好，但我并不完全赞同它们背后的理论。
考虑这种存在类型的例子：
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 ？
首先，看看“咖喱霍华德对应”，它指出计算机程序中的类型对应于直觉逻辑中的公式。 直觉逻辑就像你在学校学到的“常规”逻辑，但没有排除中等或双重否定消除的规律：
不是一个公理：P⇔¬¬P（但P⇒¬¬P很好）
不是公理：P∨¬P
逻辑规律
你与德摩根的法律是正确的，但首先我们要用它们来衍生出一些新的。 德摩根法律的相关版本是：
我们可以导出（∀x.P⇒Q（x））= P⇒（∀x.Q（x））：
和（∀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
量化类型
让我们将存在量词∃添加到我们的原始类型（第一个，没有类型构造函数）。 而不是将其引入类似于逻辑的类型定义中，而是将其引入构造函数/访问器定义中，这看起来像逻辑。 我们稍后将修复数据定义以匹配。
现在我们将使用∃x. t代替Int ∃x. t ∃x. t 。 这里， t是某种类型的表达。
Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)
根据逻辑规则（上述第二条规则），我们可以将Con的类型重写为：
Con :: ∀x. t -> T
当我们将存在量词移到外部时（prenex形式），它变成了一个通用量词。
因此，以下是理论上相同的：
data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil
除Haskell中没有exists语法外。
在非直觉逻辑中，允许从unCon的类型中推导出以下unCon ：
unCon :: ∃ T -> t -- invalid!
这是无效的原因是因为直觉主义逻辑中不允许这种转换。 因此， unCon没有exists关键字，就不可能为unCon编写类型，并且不可能将类型签名置于prenex形式。 很难让类型检查器保证在这种情况下终止，这就是为什么Haskell不支持任意存在量词的原因。
来源
“类型推理的一类多态性”Mark P. Jones，第24届ACM SIGPLAN-SIGACT关于编程语言原理（网络）
Plotkin和Mitchell在他们着名的论文中建立了存在类型的语义，这些论文在编程语言中抽象类型与逻辑中的存在类型之间建立了联系，
Mitchell，John C .; Plotkin，Gordon D. 抽象类型具有存在型，编程语言和系统ACM交易，卷。 10，第3号，1988年7月，第470-502页
在高层次上，
抽象数据类型声明以类型化编程语言出现，如Ada，Alphard，CLU和ML。 这种声明形式将一系列标识符绑定到一个带有关联操作的类型上，这个复合“值”我们称之为数据代数。 我们使用二阶类型的lambda演算SOL来显示数据代数如何给出类型，作为参数传递，并作为函数调用的结果返回。 在这个过程中，我们讨论抽象数据类型声明的语义，并回顾类型化编程语言和构造逻辑之间的联系。
它在你链接的haskell wiki文章中有说明。 我会借用一些代码和评论，并尝试解释。
data T = forall a. MkT a
在这里你有一个类型T与类型构造函数MkT :: forall a. a -> T MkT :: forall a. a -> T ，对吗？ MkT （大致）是一个函数，因此对于每种可能的类型a ，函数MkT都具有类型a -> T 因此，我们同意通过使用该构造函数，我们可以构建像[MkT 1, MkT 'c', MkT "hello"] ，它们都是T类型。
foo (MkT x) = ... -- what is the type of x?
但是当你尝试提取（例如通过模式匹配）包含在T的值时会发生什么？ 它的类型注解只能表示T ，而不涉及实际包含的值的类型。 我们只能同意这样一个事实，无论它是什么，它都会有一个（也是唯一）一个类型; 我们如何在Haskell中说明这一点？
x :: exists a. a
这只是说存在x属于的类型a 。 在这一点上，应该清楚的是，通过从MkT的定义中删除所有的forall a并明确指定包装值的类型（即exists a. a MkT ），我们就能够达到相同的结果。
data T = MkT (exists a. a)
如果你在实现的类型类中添加条件，那么底线也是一样的。
链接地址: http://www.djcxy.com/p/43441.html