Haskell中的存在类型与全局量化类型

Question

这两者之间到底有什么区别？我认为我理解存在类型的工作原理，它们就像面向对象编程中没有向下转换方式的基类。通用类型又有何不同？

- MFlamer

---

你的意思是通用的泛型编程吗？它们就像泛型一样，也可以处理非对象数据（整数、函数等）。 - AndrewC

你可能会发现我对另一个问题的回答很有用。它涵盖了与C.A. McCann以下内容相同的领域，但是起点是“RankNTypes”。 - Luis Casillas

太好了，谢谢。这个迷人的旅程似乎没有尽头。 - MFlamer

Answer 1

这里的"universal"和"existential"术语来自谓词逻辑中同名量词。全称量化通常写为∀，可以读作“对于所有”，大致意思是：在类似于“∀x. ...” 的逻辑语句中，无论你从被量化的任何事物集合中选择什么样的“x”，“...”所代表的内容都是真实的。存在量化通常写为∃，可以读作“存在”，意味着在类似于“∃x. ...” 的逻辑语句中，“...”所代表的内容对于从被量化的事物集合中取出的某个未指定的“x”是真实的。在Haskell中，被量化的事物是类型（至少忽略某些语言扩展），我们的逻辑语句也是类型，而且我们考虑的不是“真实”，而是“可以实现”。

因此，像forall a. a -> a这样的全称量化类型意味着，对于任何可能的类型"a"，我们都可以实现一个函数，其类型为a -> a。事实上，我们可以：

id :: forall a. a -> a
id x = x

由于a是普遍量化的，我们对它一无所知，因此无法以任何方式检查参数。因此，id是该类型的唯一可能函数⁽¹⁾。

在Haskell中，普遍量化是“默认”的——签名中的任何类型变量都隐含地被普遍量化，这就是为什么id的类型通常只写为a -> a。这也被称为parametric polymorphism，在Haskell中通常只称为“多态”，在其他一些语言（例如C#）中则称为“泛型”。

像exists a. a -> a这样的存在量化类型意味着，对于某个特定类型“a”，我们可以实现一个其类型为a -> a的函数。任何函数都可以，我来选一个：

func :: exists a. a -> a
func True = False
func False = True

...这当然是布尔类型上的“not”函数。但问题在于，我们不能像使用其他函数那样使用它，因为我们所知道的关于“a”类型的所有信息都已被丢弃，这意味着我们不能将func应用于任何值。

这并不是很有用。

那么我们能用func做什么呢？好吧，我们知道它是一个输入输出类型相同的函数，所以我们可以将其与自身组合。基本上，您可以对具有存在类型的东西进行的唯一操作是基于类型的非存在部分进行的操作。同样，给定类型为exists a. [a]的内容，我们可以找到它的长度，或将其连接到自身，或删除一些元素，或对任何列表可以做的其他任何事情。

那最后一点又回到了全称量词，以及 Haskell⁽²⁾ 直接没有存在类型的原因（遗憾的是，我的上面的 exists 是完全虚构的）：由于具有存在量化类型的事物只能与具有全称量化类型的操作一起使用，我们可以将类型 exists a. a 写成 forall r. (forall a. a -> r) -> r--换句话说，对于所有结果类型 r，给定一个函数，该函数针对所有类型 a 接受类型为 a 的参数并返回类型为 r 的值，我们可以获得类型为 r 的结果。

如果你不清楚它们为什么几乎等价，请注意，总体类型并不是普遍量化的 a——相反，它接受一个自身对 a 全称量化的参数，然后可以将其与任何特定类型一起使用。

---

作为旁注，虽然Haskell在通常意义上没有子类型的概念，但我们可以将量词视为表达一种形式的子类型，层次结构从普遍到具体到存在。类型为forall a. a的某些内容可以转换为任何其他类型，因此它可以被视为一切的子类型；另一方面，任何类型都可以转换为类型exists a. a，使其成为所有内容的父类型。当然，前者是不可能的（除了错误之外，不存在类型为forall a. a的值），后者是无用的（您不能对类型exists a. a做任何事情），但类比至少在纸上有效。请注意，存在类型和普遍量化的参数之间的等价性之所以成立，是因为variance在函数输入方面翻转的原因。

---

因此，基本思想大致是：全称量化类型描述适用于任何类型的相同事物，而存在量化类型描述适用于特定但未知类型的事物。

---

1: 嗯，并非完全如此——只有当我们忽略会导致错误的函数（例如notId x = undefined）以及永远不会终止的函数（例如loopForever x = loopForever x）时才是这样。

2: 嗯，GHC。没有扩展功能，Haskell 只有隐式全称量词，完全没有谈论存在类型的实际方法。

- C. A. McCann

---

谢谢您出色的解释。我有一个疑问：您已经说明了存在a.a和对于所有r. (对于所有a.a→r)->r是等价的。它们如何相等（是否有任何推导）？这是制度逻辑的结果之一吗？感谢您出色的解释。我有一个疑问：您已经说明了存在a.a和对于所有r. (对于所有a.a→r)->r是等价的。它们如何相等（是否有任何推导）？这是制度逻辑的结果之一吗？ - Sibi

是的，这本质上是将德摩根定律应用于量词；在逻辑上来说，函数输入被否定了。Either a b 和 forall r. (a -> r, b -> r) -> r 之间也存在类似的等价关系，对应于“A 或 B”与“非（非 A）且非 B”的相同性质。 - C. A. McCann

谢谢。但是 r 在这里是如何出现的呢？在最初的前提中没有 r，但是当你应用 De Morgan 定律时它是如何出现的呢？对 forall r. (forall a. a -> r) -> r 的推导将非常有帮助。再次感谢您抽出时间写出优秀的答案。 - Sibi

@Sibi: 这里的 r 代表“假”。从技术上讲，“假”应该对应一个未被占用的数据类型（通常称为 Void），但是使用 r 可以让我们取回值。因此，“非（非A）”将是 （A -> Void）-> Void（无用）或 forall r.（A -> r）-> r，它允许我们提取 A 值，即双重否定消除。如果您想了解逻辑双重否定和延续传递风格之间的联系，请查阅相关资料。 - C. A. McCann

由于对偶性，forall a. a 可以表示为 exists r. (exists a. a -> r) -> r。 - PyRulez

Answer 2

巴托什·米莱夫斯基在他的书中提供了有关为什么Haskell不需要存在量词的一些很好的见解。

in pseudo-Haskell:

(exists x. p x x) -> c ≅ forall x. p x x -> c

It tells us that a function that takes an existential type is equivalent to a polymorphic function. This makes perfect sense, because such a function must be prepared to handle any one of the types that may be encoded in the existential type. It’s the same principle that tells us that a function that accepts a sum type must be implemented as a case statement, with a tuple of handlers, one for every type present in the sum. Here, the sum type is replaced by a coend, and a family of handlers becomes an end, or a polymorphic function.

因此，Haskell 中存在量化类型的示例是：

data Sum = forall a. Constructor a    (i.e. forall a. (Constructor_a:: a -> Sum) ≅ Constructor:: (exists a. a) -> Sum)

可以将其视为一个总和数据类型Sum = 整数 | 字符 | 布尔 | ...。相比之下，一个在Haskell中被普遍量化的类型的示例是

data Product = Constructor (forall a. a)

可以将其视为一个产品 数据产品 = 整型 字符型 布尔型 ...。

- Tom Huntington