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

Question

这些有什么区别？我想我理解存在类型是如何工作的,它们就像在OO中拥有一个基类而没有一种方法可以用.普遍类型有何不同？

Answer 1

这里的术语"通用"和"存在主义"来自谓词逻辑中类似命名的量词.

通用量化通常写成∀,您可以将其视为"为所有人",并且大致意味着它的含义:在类似"∀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.这也称为参数多态,在Haskell中通常被称为"多态",在一些其他语言(例如,C#)中称为"泛型".

一个存在性量化的类型一样exists 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),但这个类比至少在纸上起作用.:]

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

因此,基本思想粗略地说,普遍量化的类型描述了对任何类型都相同的事物,而存在类型描述了使用特定但未知类型的事物.

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

2:嗯,GHC.没有扩展,Haskell只有隐含的通用量词,根本没有真正谈论存在类型的方法.

Answer 2

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

\n

\n

在伪 Haskell 中：

\n

(exists x. p x x) -> c \xe2\x89\x85 forall x. p x x -> c\n

\n

它告诉我们，采用存在类型的函数相当于多态函数。这是完全有道理的，因为这样的函数必须准备好处理可能在存在类型中编码的任何一种类型。它\xe2\x80\x99 的原理相同，告诉我们接受 sum 类型的函数必须作为 case 语句实现，并带有一组处理程序，每个处理程序对应 sum 中存在的每种类型。在这里，sum 类型被 coend 取代，并且一系列处理程序成为 end 或多态函数。

\n

\n

因此，Haskell 中存在量化类型的一个例子是

\n

data Sum = forall a. Constructor a    (i.e. forall a. (Constructor_a:: a -> Sum) \xe2\x89\x85 Constructor:: (exists a. a) -> Sum)\n

\n

可以将其视为 sum\n data Sum = int | char | bool | ...。相比之下，Haskell 中通用量化类型的示例是

\n

data Product = Constructor (forall a. a)\n

\n

这可以被视为一种产品data Product = int char bool ...。

\n