haskell - 使用 RankNTypes 编码 ExistentialQuantification

Question

我在几个地方读到声称可以使用 ExistentialQuantification 获得与 RankNTypes 等效的功能。有人可以举例说明为什么这是可能的或不可能的吗？

Answer 1

通常，Haskell 中的所有类型变量都在类型的最外层范围内隐式地通用量化。 RankNTypes 允许通用量词 forall 出现嵌套，例如forall a b. (a -> a) -> b -> b 类型与 forall b. (forall a. a -> a) -> b -> b 非常不同。

在某种意义上，函数箭头左侧的类型在逻辑上是“否定的”，大致与 (->) 是逻辑蕴涵的意义相同。从逻辑上讲，全称量词和存在量词通过德摩根对偶相关联:(∃x.P(x)) 等价于 ¬(∀x. ¬P(x))，或者换句话说“存在一个 x 使得P(x)”对应于“对于所有 x，P(x) 不是假的”。

因此，函数箭头左侧的 forall 被“否定”并且表现得像一个存在。如果你把整个东西放在另一个函数箭头的左边，它会被双重否定并再次充当全称量词，对一些繁琐的细节进行模数。

否定的相同想法也适用于值，因此要对我们想要的 exists x. x 类型进行编码:

forall x. 在逆变(否定)位置

在协变(正)位置的该类型的值 x。

由于值必须在量词的范围内，我们唯一的选择是双重否定——基本上是 CPS 变换。为了避免以其他方式限制事物，我们将通用量化函数箭头右侧的类型。所以 exists x. x 被翻译成 forall r. (forall x. x -> r) -> r 。将此处的类型和量词的位置与上述要求进行比较，以验证它是否满足要求。

在更多的操作术语中，这只是意味着给定一个具有上述类型的函数，因为我们给它一个具有通用量化参数类型的函数，它可以将该函数应用于它喜欢的任何类型 x，并且因为它没有其他方法可以得到 r 类型的值，我们知道它将将该函数应用于某些东西。所以 x 将指代某种类型，但我们不知道是什么——这基本上是存在量化的本质。

在更实际的日常术语中，如果您从函数类型的“另一面”来看，任何普遍量化的类型变量都可以被视为存在。由于作为类型推断的一部分执行的统一超越了量词范围，因此有时最终会出现 GHC 必须将外部范围中的类型变量与嵌套范围中的量化类型统一的情况，这就是您获得编译器错误的方式关于转义类型和 skolems 等等，后者(我假设)与 Skolem normal form 相关。

这与使用existentials的数据类型相关的方式是，虽然您可以声明这样的类型:

data Exists = forall a. Exists a

这表示存在类型，要获得“存在类型”，您需要通过模式匹配将其解包:

unexist :: Exists -> r
unexist (Exists x) = foo x

但是如果你考虑在这个定义中 foo 的类型，你最终会得到类似 forall a. a -> r 的东西，它相当于上面的 CPS 风格的编码。 CPS 转换和数据类型的 Church 编码之间有着密切的关系，因此 CPS 形式也可以看作是模式匹配的具体化版本。

最后，将事情与逻辑联系起来——因为这就是术语“存在量词”的来源——请注意，如果你认为左箭头是否定并且有点眯着眼忽略 forall r. ... CPS cruft，这些存在的编码类型与作为起点的 De Morgan 二元化形式 ¬(∀x. ¬P(x)) 完全相同。所以这些实际上都是看待同一概念的不同方式。