为啥存在量化的 Haskell 中没有“Exist”关键字？

Posted 2023-03-28

【中文标题】为啥存在量化的 Haskell 中没有“Exist”关键字？

【英文标题】：Why there is no an "Exist" keyword in Haskell for Existential Quantification?为什么存在量化的 Haskell 中没有“Exist”关键字？

【发布时间】：2015-02-16 16:05:50

【问题描述】：

根据 GHC 文档，给出以下声明：

data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

然后

MkFoo :: forall a. a -> (a -> Bool) -> Foo

与以下伪 Haskell 声明（几乎）同构

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

因此，不需要单独的“Exist”关键字。因为：

Haskell 程序员可以安全地普遍考虑平凡 上面给出的量化类型。

但我不确定这意味着什么。谁能解释一下为什么我们可以使用全称量词来表达存在量词？

【参考方案1】：

在逻辑（经典或直觉）中，公式

(exists x. p x) -> q
forall x. (p x -> q)

是等价的（注意q 不依赖于上面的x）。这可以用来用全称量化来表达存在量化，前提是存在存在于蕴涵的左侧。 （这里是经典的proof。）

在函数式编程中，您可以实现相同的目的。而不是写

-- Pseudo-Haskell follows
f :: (exists a. (a, a->Int)) -> Int
f (x,h) = h x

我们可以使用

-- Actual Haskell
f :: forall a. (a, a->Int) -> Int
f (x,h) = h x

所以我们可以不用存在量化，至少在上述情况下。

当它不在箭头左侧时，仍然需要存在量化。例如，

g :: exists a. (a, a->Int)
g = (2 :: Int, \x -> x+3)

唉，Haskell 选择不包含这些类型。可能是为了防止已经复杂的类型系统变得过于复杂。

尽管如此，Haskell 得到了存在数据类型，它只需要围绕存在包装/解包一个构造函数。例如，使用 GADT 语法，我们可以这样写：

data Ex where
  E :: forall a. (a, a->Int) -> Ex
g :: Ex
g = E (2 :: Int, \x -> x+3)

最后，让我补充一点，existentials 也可以通过 rank-2 类型和 continuation-passing 来模拟：

g :: forall r. (forall a. (a, a->Int) -> r) -> r
g k = k (2 :: Int, \x -> x+3)

【讨论】：

您能否添加推导步骤以了解(exists x. p x) -> q 和forall x. (p x -> q) 如何等效？我很难用经典逻辑定律来弄清楚。

您可以在 Haskell 中“证明”等价性：data Ex (p :: * -> *) where Ex :: p x -> Ex p 和 iso1 :: (Ex p -> q) -> (forall x . p x -> q); iso1 f a = f (Ex a) iso2 :: (forall x . p x -> q) -> (Ex p -> q); iso2 f (Ex a) = f a。 “经典”证明可以在question的答案中找到。

【参考方案2】：

首先要注意的是 forall 量词出现在等号的右侧，因此它与 数据构造函数（不是类型）相关联：MkFoo .因此，Foo 类型没有说明 a。

当我们尝试对Foo 类型的值进行模式匹配时，我们再次遇到a。到那时，您对MkFoo 的组件几乎一无所知，除了它们存在（必须存在用于调用MkFoo 的类型）并且可以使用第一个组件作为第二个组件的参数，它是一个函数：

f :: Foo -> Bool
f (MkFoo val fn) = fn val

【参考方案3】：

如果您查看数据构造函数的类型，您会注意到我们同样使用-> 来表示产品。例如

(:) :: a -> [a] -> [a]

实际上意味着我们使用(:) 来打包a与[a] 类型的列表并传递[a] 类型的列表。

在你的例子中，forall 的使用仅仅意味着MkFoo，作为一个构造函数，愿意打包任何类型的a。当您阅读 GHC 文档中的 (exists a . (a, a -> Bool)) -> Foo 时，您应该将其视为原始类型 MkFoo 的非咖喱版本。 (:) 的相应非咖喱版本将是 (a, [a]) -> [a]。