为什么在Haskell中存在用于存在量化的"存在"关键字？

Question

根据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

因此,不需要分离的"存在"关键字.因为:

Haskell程序员可以安全地考虑上面给出的普通的通用量化类型.

但我不确定这意味着什么.有人可以解释一下,为什么我们可以使用通用量词来表达存在量化？

Answer 1

在逻辑(经典或直觉)中,公式

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

是等价的(注意,q不依赖于x上述).这可以用来表达存在主义量化的普遍量化,前提是存在主义在左侧隐含着意义.(这是一个经典的证据.)

在函数式编程中,您可以实现相同的功能.而不是写作

-- 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)

最后,让我补充一点,存在性也可以通过rank-2类型和continuation-passing来模拟:

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