我在一些地方读到过声称ExistentialQuantification可以使用RankNTypes. 有人可以举例说明为什么这是或不可能的吗？
问问题
563 次
2 回答
11
通常，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我们想要的类型：
forall x.在逆变（否定）位置- 该类型的值
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)) 完全相同。所以这些实际上都是看待同一个概念的不同方式。
于 2013-01-24T00:29:18.303 回答
3
于 2013-01-24T02:31:33.607 回答