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

我开始了解如何在所谓的“现有类型”中使用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的东西...

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

他们不完整。他们解释了该关键字使用的一部分(如“existential types”)，这使我感到高兴，直到我阅读了以完全不同的方式使用它的代码(如上述的runST，foo和bar)。

他们密密麻麻地假定我在本周流行的离散数学，范畴论或抽象代数的任何分支中都读到了最新的文章。 (如果我再也没有读过“请咨询论文以了解实现细节”这句话，那就太早了。)

它们的编写方式经常将甚至简单的概念变成曲折而 splinter 的语法和语义。

所以...

关于实际问题。有人可以用清晰，简洁的英语完全解释forall关键字(或者，如果它存在于某处，则指向我错过的如此清晰的解释)，而不假定我是一个深深地扎在行话中的数学家吗？

编辑添加:

以下是较高质量的答案中有两个突出的答案，但是不幸的是，我只能选择其中一个作为最佳答案。 Norman's answer详尽且有用，它以某种方式解释了事物，从而显示了forall的一些理论基础，同时向我展示了它的一些实际含义。 yairchu's answer覆盖了一个没人提及的区域(作用域类型变量)，并通过代码和GHCi session 说明了所有概念。我会尽可能地选择两者。不幸的是，我无法这样做，在仔细查看了两个答案之后，由于示例性代码和附加的解释，我认为yairchu的语言略微超出了Norman的语言。但是，这有点不公平，因为我确实需要两个答案才能理解这一点，以至于forall在类型签名中看到它时不会让我感到恐惧。

最佳答案

让我们从一个代码示例开始:

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-Type有什么不同？

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

对于Rank-N-Types，forall a表示您的表达式必须适合所有可能的a。例如:

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

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

因此，对于Existential-Quantification，forall定义中的data s意味着，所包含的值可以是任何合适的类型，而不是必须是所有适合的类型。

关于haskell - Haskell/GHC中的 `forall`关键字有什么作用？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/3071136/

forAll

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