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。

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

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

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

1. forall x.在逆变（否定）位置
2. 该类型的值x在协变（正）位置。

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

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

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

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

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，这些存在类型的编码与作为起点的德摩根二元形式 ¬(∀x. ¬P(x)) 完全相同。所以这些实际上都是看待同一个概念的不同方式。

Answer 2