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

【问题标题】：What's the theoretical basis for existential types?存在类型的理论基础是什么？
【发布时间】：2012-05-31 22:58:00
【问题描述】：

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？

我能想到的最接近的事情是逻辑上的De Morgan's Laws，其中交换否定和量词的顺序将存在量词变成全称量词，反之亦然：

¬(∀x. px) ⇔ ∃x. ¬(px)

但数据构造函数似乎与否定运算符完全不同。

使用forall 而不是不存在的exists 定义存在类型的能力背后的理论是什么？

【问题讨论】：

标签： haskell types type-systems existential-type quantifiers

【解决方案1】：

首先，看一下“Curry Howard 对应”，它指出计算机程序中的类型对应于直觉逻辑中的公式。直觉逻辑就像你在学校学到的“常规”逻辑，但没有排中律或双重否定排除法：

不是公理：P ⇔ ¬¬P（但 P ⇒ ¬¬P 很好）
不是公理：P ∨ ¬P

逻辑法则

您在 DeMorgan 定律的正确轨道上，但首先我们将使用它们推导出一些新的定律。德摩根定律的相关版本是：

∀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)

And (∀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

量化类型

让我们将存在量词∃添加到我们的原始类型（第一个，没有类型构造函数）。与其在看起来不像逻辑的类型定义中引入它，不如在看起来像逻辑的构造函数/访问器定义中引入它。我们稍后会修复数据定义以匹配。

我们现在将使用∃x. t，而不是Int。这里，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!

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

来源

“First-class Polymorphism with Type Inference”，Mark P. Jones，第 24 届 ACM SIGPLAN-SIGACT 编程语言原则研讨会论文集 (web)

【讨论】：

非常正确，已修复。从“P ∧ ¬P”推导出矛盾非常容易，因为“P ∧ ¬P”通常用作矛盾本身的定义。
干杯。如果可以的话，双重否定消除和排中是等价的，所以经典逻辑的公理只提到其中之一。严格来说，它们也等价于皮尔士定律，它具有仅使用逻辑蕴涵的良好特性（该定律如下：((P ⇒ Q) ⇒ P) ⇒ P)。皮尔士定律与call/cc 有 CH 对应关系。
值得一提的是，如果您将存在视为（弱）依赖对，那么您从 Con :: (∃x. t) -> T 到 Con :: ∀x. t -> T 的转换只是柯里化。
@DietrichEpp：依赖对在 CH 下编码存在量化。例如，(∃n) n + 1 = 2 将被编码为Σ[ n ∶ ℕ ] (n + 1 ≡ 2)，则证明由见证人和见证人满足命题的证明组成，例如(1 , refl)（您可以将refl读作“遵循定义")。将其与编码通用量化的相关函数进行比较。 (n : ℕ) → n ≡ 0 + n 类型的函数将任意自然数转换为 n = 0 + n 的证明。
我相信你应该声明 Not a theorem: P ⇔ ¬¬P 等等。它是否是公理并不重要，重要的是它不是直觉逻辑的定理。

【解决方案2】：

Plotkin 和 Mitchell 在他们的著名论文中为存在类型建立了语义，它在编程语言中的抽象类型和逻辑中的存在类型之间建立了联系，

米切尔，约翰 C.；普洛特金，戈登 D。 Abstract Types Have Existential Type，ACM 编程语言和系统交易，卷。 10, 第 3 期，1988 年 7 月，第 470-502 页

在高层次上，

抽象数据类型声明出现在 Ada、Alphard、CLU 和 ML 等类型化编程语言中。这种形式的声明将标识符列表绑定到具有相关操作的类型，a 我们称之为数据代数的复合“值”。我们使用二阶类型 lambda 演算 SOL 以显示数据代数如何被赋予类型，作为参数传递，并作为函数调用的结果返回。在过程中，我们讨论抽象数据类型的语义声明和审查类型化编程之间的联系语言和建设性逻辑。

【讨论】：

【解决方案3】：

它在您链接的haskell wiki文章中有所说明。借用几行代码和cmets来解释一下。

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

这只是说存在x 所属的类型a。此时应该清楚的是，通过从MkT 的定义中删除forall a 并明确指定包装值的类型（即exists a. a），我们能够获得相同的结果。

data T = MkT (exists a. a)

如果您像示例中那样在已实现的类型类上添加条件，底线也是相同的。

【讨论】：