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

Question

这些到底有什么区别呢？我想我理解存在类型是如何工作的，它们就像OO中的基类没有向下强制转换的方法一样。通用类型有何不同？

Answer 1

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

通用量化通常被写成“have”，你可以读成“for all”，大致意思是它听起来像什么：在一个类似于“have x...”的逻辑语句中，无论“...”的位置是什么对于所有可能的“x”都是真的，你可以从任何被量化的东西中选择。

存在量化通常被写成“存在”，您可以将其读作“存在”，这意味着在类似于“存在x...”的逻辑语句中，无论“...”的位置是什么对于从被量化的事物集合中提取的一些未指定的“x”来说是正确的。

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

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

在Haskell中，通用量化是“默认的”--签名中的任何类型变量都隐式地通用量化，这就是为什么ID的类型通常只写为a->a。这也被称为参数多态性，在Haskell中通常被称为“多态性”，在其他一些语言（例如C#)中被称为“泛型”。

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

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

最后一点让我们回到了通用量词，而Haskell⁽²⁾没有直接具有存在类型的原因（我的exists完全是虚构的，唉）：因为具有存在量化类型的东西只能与具有通用量化类型的操作一起使用，所以我们可以编写exists类型。将用作所有R的。（对于所有a.a->r)->r--换句话说，对于所有结果类型r，给定一个函数，对于所有类型a接受a类型的参数并返回r类型的值，我们可以得到r类型的结果。

如果您不清楚为什么它们几乎等价，请注意，对于A，整体类型并不是普遍量化的--相反，它接受了一个参数，该参数本身对于A是普遍量化的，然后它可以将该参数用于它选择的任何特定类型。

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

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

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

1：嗯，不完全是--只有当我们忽略导致错误的函数时，比如notid x=undefined，包括从不终止的函数，比如loopForever x=loopForever x。

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