haskell - Haskell/GHC 中的 `forall` 关键字有什么作用？

Question

我开始理解 forall 关键字如何在所谓的“存在类型”中使用，如下所示:

data ShowBox = forall s. Show s => SB s

然而，这只是 forall 的使用方式的一个子集，我根本无法理解它在这样的事情中的使用:

runST :: forall a. (forall s. ST s a) -> a

或者解释为什么它们不同:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

或者整个RankNTypes内容...

我倾向于更喜欢清晰、无行话的英语，而不是学术环境中常见的语言。我尝试阅读的大多数解释(我可以通过搜索引擎找到的解释)都存在以下问题:

1. 它们不完整。他们解释了此关键字的一部分用法(例如“存在类型”)，这让我感到很高兴，直到我读到以完全不同的方式使用它的代码(例如 runST、foo 和 bar 上面)。
2. 其中充满了这样的假设:我已经阅读了本周流行的离散数学、范畴论或抽象代数的任何分支的最新内容。 (如果我再也没有读过“无论怎样，请参阅论文以获取实现细节”这句话，那就太早了。)
3. 它们的编写方式常常会将简单的概念变成曲折扭曲、支离 splinter 的语法和语义。

所以...

关于实际问题。任何人都可以用清晰、简单的英语完全解释 forall 关键字(或者，如果它存在于某个地方，请指出我错过的这样一个清晰的解释)，并且不假设我是一名数学家用行话来说？

Answer 1

让我们从代码示例开始:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

此代码无法在普通 Haskell 98 中编译(语法错误)。它需要扩展来支持 forall关键字。

基本上，forall 有 3 种不同常见用途关键字(或者至少看起来如此)，并且每个关键字都有自己的 Haskell 扩展:ScopedTypeVariables , RankNTypes/Rank2Types , ExistentialQuantification .

上面的代码在启用其中任何一个的情况下都不会出现语法错误，但仅使用 ScopedTypeVariables 进行类型检查。已启用。

作用域类型变量:

作用域类型变量有助于指定 where 内代码的类型条款。它使得b在val :: b与 b 相同在foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b .

一个令人困惑的点:当您省略 forall 时，您可能会听到这一点。从类型来看，它实际上仍然隐式存在。 (from Norman's answer: "normally these languages omit the forall from polymorphic types")。此声明是正确的，但它指的是 forall 的其他用途，而不是ScopedTypeVariables使用。

排名-N-类型:

让我们从mayb :: b -> (a -> b) -> Maybe a -> b开始相当于 mayb :: forall a b. b -> (a -> b) -> Maybe a -> b ，除了，当 ScopedTypeVariables 时已启用。

这意味着它适用于每个 a和b .

假设您想做这样的事情。

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

这个 liftTup 的类型必须是什么？这是liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b) 。要了解原因，让我们尝试编写代码:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

“嗯..为什么 GHC 推断元组必须包含两个相同类型？让我们告诉它它们不必是”

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

嗯。所以这里 GHC 不允许我们申请 liftFunc上v因为v :: b和liftFunc想要一个x 。我们确实希望我们的函数能够接受任何可能的 x !

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

所以这不是liftTup适用于所有人 x ，这是它得到的函数的作用。

存在量化:

让我们举个例子:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

这与 Rank-N-Types 有什么不同？

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

对于 Rank-N-类型，forall a意味着你的表达必须符合所有可能的a s。例如:

ghci> length ([] :: forall a. [a])
0

空列表可以用作任何类型的列表。

因此，对于存在量化，forall位于data定义意味着，包含的值可以是任何合适的类型，而不是它必须是所有合适的类型类型。