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

Question

Haskell Wiki讲解了如何使用存在类型的相关知识，但我还不太理解它们背后的理论。

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

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

定义一个类型包装器，用于可以转换为String的内容。Wiki提到我们想要定义的实际上是像这样的一种类型：

为可以转换为String的内容定义一个类型包装器。维基百科提到，我们实际上想要定义的是像这样的一种类型：

data S = S (exists a. Show a => a)    -- (2)

也就是一个真正的“存在”类型——我认为可以大致理解为说“数据构造函数 S 可以接受任何具有Show实例的类型，并将其封装起来”。事实上，你可以像下面这样编写一个GADT：

```haskell data SomeShow where S :: Show a => a -> SomeShow ``` ```

data S where                          -- (3)
    S :: Show a => a -> S

我还没有尝试编译它，但看起来应该可以工作。对我来说，GADT 显然相当于我们想要编写的代码（2）。

但是，对我来说完全不明显为什么（1）等同于（2）。为什么将数据构造函数移到外部会将 forall 转换为 exists？

我能想到最接近的东西是逻辑中的 德摩根定律 ，在其中，交换否定和量词的顺序可以将存在量词转换为全称量词，反之亦然：

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

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

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

- Chris Taylor

Answer 1

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

• 不是公理：P ⇔ ¬¬P（但 P ⇒ ¬¬P 是可以的）

• 不是公理：P ∨ ¬P

逻辑定律

DeMorgan定律是正确的，但首先我们将使用它们来推导出一些新的定律。 DeMorgan定律的相关版本如下：

• ∀x. P(x) = ¬∃x. ¬P(x)
• ∃x. P(x) = ¬∀x. ¬P(x)

我们可以推导出 (∀x. P ⇒ Q(x))  =  P ⇒ (∀x. Q(x))：

1. (∀x. P ⇒ Q(x))的意思是对于任何x，如果P成立，则Q(x)也成立。
2. (∀x. ¬P ∨ Q(x))的意思是对于任何x，如果P不成立，则Q(x)成立。
3. ¬P ∨ (∀x. Q(x))的意思是如果P不成立，则对于任何x，Q(x)都成立；或者P成立。
4. P ⇒ (∀x. Q(x))的意思是如果P成立，则对于任何x，Q(x)都成立。

而且(∀x. Q(x) ⇒ P)  =  (∃x. Q(x)) ⇒ P (下面会用到):

1. (∀x. Q(x) ⇒ P)的意思是对于任何x，如果Q(x)成立，则P也成立。
2. (∀x. ¬Q(x) ∨ P)的意思是对于任何x，如果Q(x)不成立，则P成立。
3. (¬¬∀x. ¬Q(x)) ∨ P的意思是对于任何x，如果Q(x)不成立，则P成立。
4. (¬∃x. Q(x)) ∨ P的意思是如果不存在x使得Q(x)成立，则P成立。
5. (∃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的类型，并且无法将类型签名放在前尼可斯范式中。在这种情况下，很难制作一个保证终止的类型检查器，这就是为什么Haskell不支持任意存在量词的原因。

来源

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

- Dietrich Epp

---

非常正确，已修正。从“P ∧ ¬P”中推导出矛盾非常容易，因为“P ∧ ¬P”通常被用作矛盾本身的定义。 - Dietrich Epp

好的。如果可以的话，双重否定消除和排中律是等价的，因此经典逻辑公理只提到了其中一个。严格来说，它们也等价于皮尔斯定律，该定律具有仅使用逻辑蕴涵的良好属性（该定律如下：((P ⇒ Q) ⇒ P) ⇒ P）。皮尔斯定律与call/cc具有CH对应关系。 - Vitus

值得一提的是，如果您将存在类型视为（弱）依赖对，则从Con :: (∃x. t) -> T到Con :: ∀x. t -> T的转换只是柯里化。 - copumpkin

@DietrichEpp：依赖对编码 CH 下的存在量化。例如，(∃n) n + 1 = 2 将被编码为 Σ[ n ∶ ℕ ] (n + 1 ≡ 2)，证明由证人和证明证人满足命题组成，例如 (1 , refl)（可以将 refl 理解为“根据定义”）。与依赖函数相比，它们编码普遍量化。类型为 (n : ℕ) → n ≡ 0 + n 的函数将任意自然数转换为一个证明，证明 n = 0 + n。 - Vitus

我曾经很难非正式地理解 ∀x. (Q(x) ⇒ P) ⇔ ∃x. Q(x) ⇒ P。我会这样翻译它：对于所有的x：如果x是一只红色的猫，那么汉斯就会害怕。 ⇔ 如果至少存在一只红色的猫，那么汉斯就会害怕。 所以 Q(x) = x 是一只红色的猫？ 而 P = 汉斯害怕。 这让我明白了。不确定是否能帮到其他人。 - hasufell

Answer 2

Plotkin和Mitchell在他们著名的论文中为存在类型建立了一个语义，将编程语言中的抽象类型与逻辑中的存在类型联系起来。

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

- Don Stewart

Answer 3

你链接的Haskell维基文章中有提到。我将借用其中一些代码和注释并尝试解释。

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 属于这个类型。 现在很明显，通过从 MkT 的定义中删除 forall a 并明确指定包装值的类型（即 exists a. a），我们能够达到相同的结果。

data T = MkT (exists a. a)

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

- Riccardo T.