61

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

4

2 回答 2

105

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

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

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

在 Haskell 中，被量化的东西是类型（至少忽略某些语言扩展），我们的逻辑语句也是类型，我们认为“可以实现”而不是“真实”。

所以，一个普遍量化的类型forall a. a -> a意味着，对于任何可能的类型“a”，我们可以实现一个类型为 的函数a -> a。事实上，我们可以：

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

由于a是普遍量化的，我们对此一无所知，因此无法以任何方式检查论点。该类型(1)id的唯一可能功能也是如此。

在 Haskell 中，通用量化是“默认值”——签名中的任何类型变量都被隐式地通用量化，这就是为什么类型id通常写为 just a -> a。这也称为参数多态，在 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 (2)没有直接存在类型的原因（我的exists上面完全是虚构的，唉）：因为存在量化类型的事物只能用于具有普遍量化的类型，我们可以把类型exists a. a写成forall r. (forall a. a -> r) -> r——换句话说，对于所有结果类型r，给定一个函数，对于所有类型，都a接受一个类型的参数a并返回一个类型的值r，我们可以得到一个类型的结果r。

如果你不清楚为什么它们几乎是等价的，请注意，整体类型不是普遍量化的——a而是，它需要一个本身被普遍量化的参数，a然后它可以与它选择的任何特定类型一起使用。

顺便说一句，虽然 Haskell 并没有真正意义上的子类型化概念，但我们可以将量词视为表达子类型化的一种形式，其层次结构从普遍到具体再到存在。某种类型的东西forall a. a可以转换为任何其他类型，因此它可以被视为一切事物的子类型；另一方面，任何类型都可以转换为 type exists a. a，使其成为所有内容的父类型。当然，前者是不可能的（forall a. a除了错误之外没有类型的值），而后者是无用的（你不能对 type 做任何事情exists a. a），但这个类比至少在纸面上是有效的。:]

请注意，存在类型和普遍量化参数之间的等价性与函数输入的方差翻转的原因相同。

因此，基本思想大致是，普遍量化的类型描述了对任何类型都适用的事物，而存在类型描述了适用于特定但未知类型的事物。

1：嗯，不完全——只有当我们忽略导致错误的函数时，例如notId x = undefined，包括永不终止的函数，例如loopForever x = loopForever x.

2：嗯，GHC。没有扩展，Haskell 只有隐含的全称量词，根本没有谈论存在类型的真正方式。

于 2013-01-13T02:10:52.080 回答
6

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)

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

data Product = Constructor (forall a. a)

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

于 2019-10-03T22:09:42.023 回答