Haskell 中存在与普遍量化的类型

Question

这些之间究竟有什么区别？我想我理解存在类型是如何工作的，它们就像在 OO 中有一个基类，没有办法进行向下转换。通用类型有何不同？

Answer 1

Bartosz Milewski 在他的书中对为什么 Haskell 不需要存在量词提供了一些很好的见解：

在伪 Haskell 中：

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

它告诉我们一个接受存在类型的函数等价于一个多态函数。这是非常有意义的，因为这样的函数必须准备好处理可能以存在类型编码的任何一种类型。同样的原则告诉我们，一个接受 sum 类型的函数必须以 case 语句的形式实现，并带有一个处理程序元组，每个处理程序对应于 sum 中存在的每个类型。在这里，sum 类型被一个 coend 代替，一个处理程序族成为一个 end 或多态函数。

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

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

这可以被认为是一个总和 data Sum = int | char | bool | ...。相比之下，Haskell 中的一个全称量化类型的例子是

data Product = Constructor (forall a. a)

这可以作为产品data Product = int char bool ...。

Answer 2

这里的术语“普遍”和“存在”来自predicate logic 中名称相似的量词。

Universal quantification 通常写为 ∀，您可以将其读作“for all”，大致意思是它听起来的样子：在类似于“∀x....”的逻辑语句中，任何代替“ ...”对于所有可能的“x”都是正确的，您可以从正在量化的任何一组事物中进行选择。

Existential quantification 通常写成∃，你可以读作“存在”，这意味着在类似于“∃x....”的逻辑语句中，任何代替“...”的东西都是对于取自被量化的事物集合中的一些未指定的“x”，则为 true。

在 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

...这当然是布尔值的“非”函数。但问题是我们不能使用它，因为我们所知道的类型“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 只有隐含的全称量词，根本没有谈论存在类型的真正方式。