存在类型的理论基础是什么？

Question

Haskell Wiki在解释如何使用存在主义类型方面做得很好，但我不太了解它们背后的理论。

考虑下面这个存在类型的例子：

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

为可以转换为String的事物定义类型包装器。wiki提到我们真正想要定义的是一种类型，如

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定义存在类型的能力背后是什么理论？

Answer 1

首先，看一看"Curry通信“，其中指出计算机程序中的类型与直觉逻辑中的公式相对应。直觉逻辑就像你在学校学到的“规则”逻辑，但没有排除中间否定或双重否定的规律：

• 不是公理:P，⇔，P(但P，⇒)很好)
• 不是公理:P∨

逻辑定律

你对德摩根定律的看法是正确的，但首先我们要用它们来衍生出一些新的定律。德摩根法律的相关版本如下：

• ∀x. P(x) =n-∃x.
• ∃x. P(x) =n-∀x.

我们可以导出( = x.p.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

请注意，这些定律也适用于直觉逻辑。我们导出的两个定律在下面的论文中被引用。

简单类型

最简单的类型很容易使用。例如：

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

但是在Haskell中没有exists语法。

在非直觉逻辑中，允许从unCon类型导出以下内容

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

这是无效的原因是因为在直觉逻辑中不允许这样的转换。因此，不可能在没有unCon关键字的情况下为exists编写类型，也不可能将类型签名设置为孕产形式。在这种情况下很难保证类型检查器终止，这就是Haskell不支持任意存在量词的原因。

资料来源

“具有类型推理的一级多态性”，MarkP.Jones，第24届ACM编程语言原理研讨会(网站)论文集

Answer 2

Plotkin和Mitchell在他们的著名论文中建立了存在主义类型的语义学，它把编程语言中的抽象类型和逻辑中的存在类型联系起来，

抽象类型有存在类型，关于编程语言和系统的ACM交易，第10卷，第3号，1988年7月，第47-502页

在一个高层次上，

抽象数据类型声明出现在类型化编程语言中，如Ada、Alphard、CLU和ML。这种声明形式将标识符的列表绑定到具有关联操作的类型，这是一个复合的“值”，我们称之为数据代数。我们使用二阶类型的lambda演算SOL来说明数据代数如何被赋予类型，作为参数传递，并作为函数调用的结果返回。在此过程中，我们讨论了抽象数据类型声明的语义，并回顾了类型化编程语言与构造逻辑之间的联系。

Answer 3

在你链接的haskell wiki文章中说明了这一点。我将借用一些代码和注释，并试图解释。

data T = forall a. MkT 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

这简单地说，存在一个a类型，x属于它。此时，应该清楚的是，通过从forall a的定义中删除MkT并通过显式指定包装值的类型(即exists a. a)，我们能够实现相同的结果。

data T = MkT (exists a. a)

如果在已实现的类型分类中添加条件，则底线也是相同的，就像在示例中一样。