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

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扩展：一米二氮一x，一米三氮一x/一米四氮一x，一米五氮一x。
上面的代码在启用这两个选项时都不会出现语法错误，而只会在启用ScopedTypeVariables时出现类型检查。

作用域类型变量：

作用域类型变量可以帮助用户指定where子句中代码的类型。它使val :: b中的b与foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b中的b相同。

• 令人困惑的一点 *：你可能听说过，当你从一个类型中省略了forall，它实际上仍然隐式地存在。（来自Norman的回答：“通常这些语言省略了多态类型中的forall”）。这个声明是正确的，但是它指的是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不允许我们在v上应用liftFunc，因为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

这与秩N型有何不同？

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

空列表可以作为任何类型的列表使用。
因此，对于存在-量化，data定义中的forall s意味着，所包含的值可以是任何合适的类型，而不是它必须是所有合适的类型。

有谁能用清晰易懂的英语 * 完全 * 解释forall关键字吗？

• • 不。**（好吧，也许唐·斯图尔特可以。）

以下是简单明了地解释forall的障碍：

• 它是一个量词。你必须至少有一点逻辑（ predicate 演算）才能看到全称量词或存在量词。如果你从未见过 predicate 演算或对量词感到不舒服（我见过博士资格考试期间的学生对量词感到不舒服），那么对你来说，forall没有简单的解释。
• 它是一个 * type * 量词。如果你没有看过System F，也没有写过多态类型的实践，你会发现forall令人困惑。有Haskell或ML的经验是不够的，因为通常这些语言会从多态类型中省略forall。（在我看来，这是语言设计的错误。）
• 特别是在Haskell中，forall的使用方式让我感到困惑。（我不是类型理论家，但我的工作让我接触到了很多类型理论，我对它很满意。）对我来说，混淆的主要原因是forall被用来编码一个类型，而我自己更愿意用exists来编写这个类型。这是由一个涉及量词和箭头的棘手的类型同构来证明的，每次我想理解它时，我都必须自己查找并计算出同构。

如果您对类型同构的概念感到不舒服，或者如果您没有任何思考类型同构的实践，那么forall的使用将会阻碍您。

• 虽然forall的一般概念总是相同的（绑定引入一个类型变量），不同用法的细节可能会有很大的不同。非正式英语不是解释这些变化的好工具。要真正理解发生了什么，你需要一些数学知识。在这种情况下，相关的数学知识可以在Benjamin Pierce的介绍性文本 * Types and Programming Languages * 中找到，这是一本非常好的书。

至于你的特殊例子

• runST * 应该 * 会让你头疼。更高级别的类型（对于箭头左边的所有类型）在野外很难找到。我鼓励你阅读介绍runST的文章："Lazy Functional State Threads"。这是一篇非常好的论文，它会给你一个更好的直觉，特别是对于runST类型，以及一般的更高级别的类型。解释花了几页，做得非常好，我不打算在这里压缩它。
• 考虑

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

如果我调用bar，我可以简单地选择我喜欢的任何类型a，然后我可以传递一个函数，从类型a到类型a。我可以传递函数(+1)或函数reverse。您可以将forall视为表示"我现在可以选择类型"。（挑选类型的专业术语是"示例化"。）
调用foo的限制要严格得多：foo的参数必须是多态函数。对于这种类型，我只能传递给foo的函数是id或总是发散或出错的函数，如undefined。原因是对于foo，forall在箭头的左边，因此作为foo的调用者，我不必选择a是什么，而是由foo的 * 实现 * 来选择a是什么。因为forall位于箭头的左侧，而不是像bar那样位于箭头的上方，示例化发生在函数的主体中而不是在调用点。

• • 总结：**对forall关键字的 * 完整 * 解释需要数学知识，只有学过数学的人才能理解。没有数学知识，即使是部分解释也很难理解。但也许我的部分非数学解释会有所帮助。去阅读Launchbury和Peyton Jones关于runST的文章吧!
• • 补遗：**术语"above"，"below"，"to left of"。这些与编写类型的 * text * 方式无关，而与抽象语法树有关。在抽象语法中，forall接受类型变量的名称，然后在forall的"below"有一个完整的类型。一个箭头接受两种类型（参数和结果类型）并形成一个新的类型（函数类型）。参数类型在箭头的"to left";它是抽象语法树中箭头的左子。

示例：

• 在forall a . [a] -> [a]中，forall位于箭头上方;箭头左边的是[a]。
• 在

forall n f e x . (forall e x . n e x -> f -> Fact x f) 
              -> Block n e x -> f -> Fact x f

括号中的类型将被称为"箭头左侧的forall"（我在我正在开发的优化器中使用了类似的类型）。

我最初的回答是：
有谁能用清晰明了的英语完整地解释一下forall关键字吗
正如Norman所指出的，很难对类型论中的一个技术术语给予一个清晰、简单的英语解释，尽管我们都在努力。
关于“for all”，只有一件事需要记住：它将类型绑定到某个作用域。一旦你理解了这一点，一切都相当容易。它在类型级别上等价于'lambda'（或'let'的一种形式）-- Norman Ramsey在他的精彩回答中使用了“left”/“above”的概念来表达这个相同的作用域概念。
“forall”的大多数用法非常简单，您可以在GHC用户手册S7.8中找到介绍，尤其是关于嵌套形式“forall”的优秀S7.8.5。
在Haskell中，当类型被普遍量化时，我们通常不使用类型绑定器，如下所示：

length :: forall a. [a] -> Int

相当于：

length :: [a] -> Int

就是这样。
既然你现在可以将类型变量绑定到某个作用域，你就可以拥有除顶层（“通用量化”）之外的作用域，就像你的第一个例子，其中类型变量只在数据结构中可见，这就允许隐藏类型（“存在类型”），或者我们可以拥有任意的绑定嵌套（“秩N类型”）。
为了深入理解类型系统，你需要学习一些术语。这是计算机科学的本质。然而，像上面这样简单的用法，应该能够通过在值级别上与“let”进行类比而直观地掌握。Launchbury and Peyton Jones是一个很好的介绍。

这里有一个简单明了的快速而肮脏的解释，你可能已经很熟悉了。
在Haskell中，forall关键字实际上只有一种用法，当你看到它时，它总是意味着同样的事情。

普遍量化

• 通用量化类型 * 是forall a. f a形式的类型。该类型的值可以被认为是函数，该函数以类型a作为其参数，并返回类型f a的值。除了在Haskell中这些类型参数由类型系统隐式传递。此“函数”必须给予你相同的值，不管它接收到什么类型，所以这个值是 * 多态 * 的。

例如，考虑类型forall a. [a]，该类型的值接受另一个类型a，并返回相同类型a的元素列表，只有一种可能的实现，当然，它必须给予你一个空列表，因为a可以是任何类型，空列表是元素类型中唯一多态的列表值（因为它没有元素）。
或者forall a. a -> a类型，这样一个函数的调用者提供a类型和a类型的值，然后实现必须返回相同类型a的值，这里也只有一个可能的实现，它必须返回给定的相同值。

存在量化

一个 * 存在量化类型 * 将具有exists a. f a的形式，如果Haskell支持这种表示法的话。这种类型的值可以被认为是一个由a类型和f a类型的值组成的对（或“乘积”）。
例如，如果你有一个exists a. [a]类型的值，你有一个某种类型的元素列表，它可以是任何类型，但是即使你不知道它是什么，你也可以对这样的列表做很多事情，你可以反转它，或者你可以计算元素的数量，或者执行任何其他不依赖于元素类型的列表操作。
好的，等一下，为什么Haskell使用forall来表示一个“存在”类型，如下所示？

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

这可能会让人感到困惑，但它实际上描述了数据构造函数 * SB的 * 类型：

SB :: forall s. Show s => s -> ShowBox

一旦构造了ShowBox类型的值，你可以认为它由两个部分组成：s类型和s类型的值，换句话说，它是一个存在量化类型的值。ShowBox可以写成exists s. Show s => s，如果Haskell支持这种表示法的话。

和朋友们

既然如此，这些有什么不同？

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

我们先来看看bar，它有一个a类型和一个a -> a类型的函数并且产生一个(Char, Bool)类型的值，我们可以选择Int作为a，并且给予它一个Int -> Int类型的函数，但是foo是不同的。它要求foo的实现能够传递任何类型给我们给予它的函数，所以我们唯一可以合理地给它的函数是id。
现在我们应该能够理解runST类型的含义了：

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

所以runST必须能够产生一个类型为a的值，不管我们给予a什么类型的值，为了达到这个目的，它使用了一个类型为forall s. ST s a的参数，这个参数肯定会产生a，而且，它必须能够产生类型为a的值，而不管runST的实现决定给予什么类型作为s。
因此，实际上runST函数是在告诉您：“你可以选择a类型，只要我可以选择s类型。”
好吧，那又怎样呢？好处是这给runST的调用者设置了一个约束，因为类型a根本不能包含类型s，因为你不知道s是什么类型，你不能给它传递一个类型ST s [s]的值，实际上，这意味着runST的实现可以知道任何涉及s类型的值对于它自己的实现来说都是局部的，因此它可以自由地做否则不允许它做的事情，比如在适当的地方改变它们。类型保证了改变是局部的runST的实现。
runST的类型是 * 秩-2多态类型 * 的示例，因为其参数的类型包含forall限定符。上面foo的类型也是秩-2。普通多态类型（如bar）是秩-1，但如果参数的类型要求是多态的，则它变为秩-2。有自己的forall量词。如果一个函数使用秩为2的参数，那么它的类型是秩为3的，以此类推。一般来说，一个使用秩为n的多态参数的类型的秩为n + 1。

它们密密麻麻地塞满了假设，说明我已经读过本周流行的离散数学、范畴论或抽象代数的最新分支（如果我再也不读“查阅论文了解实现细节”这句话，那就太快了）。
呃，那么简单的一阶逻辑呢？forall很明显是指universal quantification，在这种情况下，术语existential也更有意义。尽管如果存在exists关键字则不会那么尴尬。量词是普遍的还是存在的，取决于量词相对于变量在词的哪一侧使用的位置。一个功能箭头，这有点混乱。
所以，如果这没有帮助，或者你只是不喜欢符号逻辑，从更函数化编程的Angular 来看，你可以把类型变量看作是函数的（隐式的）type 参数，在这种意义上，带类型参数的函数不管出于什么原因，传统上都是用大写的lambda来写的，我在这里写为/\。
因此，考虑id函数：

id :: forall a. a -> a
id x = x

我们可以将其重写为lambdas，将“type parameter”从类型签名中移除，并添加内联类型注解：

id = /\a -> (\x -> x) :: a -> a

下面是对const执行的相同操作：

const = /\a b -> (\x y -> x) :: a -> b -> a

因此，您的bar函数可能如下所示：

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

注意，作为参数提供给bar的函数类型取决于bar的type参数，请考虑是否使用类似以下的函数：

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

这里bar2将函数应用于Char类型的对象，因此为bar2提供Char以外的任何类型参数都会导致类型错误。
另一方面，foo可能如下所示：

foo = (\f -> (f Char 't', f Bool True))

与bar不同，foo实际上根本不接受任何类型参数！它接受一个本身接受类型参数的函数，然后将该函数应用于两个不同的类型。
因此，当您在类型签名中看到forall时，只需将其视为类型签名的lambda表达式。就像常规lambda一样，forall的作用域尽可能向右扩展，直到包含括号，并且就像在常规lambda中绑定的变量一样，由forall绑定的类型变量仅在量化表达式的作用域中。

• 后记 *：也许你会想--既然我们考虑了函数接受类型参数，为什么我们不能对这些参数做一些比把它们放入类型签名更有趣的事情呢？答案是我们可以！

把类型变量和标签放在一起并返回一个新类型的函数是一个 type constructor，你可以这样写：

Either = /\a b -> ...

但是我们需要全新的符号，因为像Either a b这样的类型的编写方式已经暗示了“将函数Either应用于这些参数”。
另一方面，一个函数在其类型参数上进行某种“模式匹配”，为不同的类型返回不同的值，这是一个类型类 * 的 * 方法。稍微扩展一下我上面的/\语法，可以得出如下结论：

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

我个人更喜欢 haskell 的语法...
“模式匹配”其类型参数并返回任意现有类型的函数是 * 类型族 * 或 * 函数依赖项 *--在前一种情况下，它甚至看起来已经非常像函数定义。

有谁能用清晰明了的英语完整地解释forall关键字（或者，如果它存在于某个地方，指出我错过的一个如此清晰的解释），而不假设我是一个沉浸在行话中的数学家？
我将尝试解释forall在Haskell及其类型系统上下文中的含义和应用。
但是在你理解之前，我想让你看一个Runar Bjarnason的演讲，题目是“Constraints Liberate, Liberties Constrain“。演讲中充满了来自真实的世界用例的例子以及Scala中的例子来支持这一说法，尽管它没有提到forall。我将在下面尝试解释forall的观点。

CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

理解并相信这句话是非常重要的，所以我敦促你观看演讲（至少是部分）。
下面是一个非常常见的例子，展示了Haskell类型系统的表达能力：
foo :: a -> a
据说，给定这种类型签名，只有一个函数可以满足这种类型，那就是identity函数或更广为人知的id。
在我学习Haskell的开始阶段，我一直想知道以下功能：

foo 5 = 6

foo True = False

它们都满足上面的类型签名，那么为什么Haskell的人声称只有id满足类型签名呢？
这是因为在类型签名中隐藏了一个隐式的forall，实际的类型是：

id :: forall a. a -> a

所以，现在让我们回到声明：束缚释放，自由束缚
将其转换为类型系统，此语句变为：

类型级别的约束变成术语级别的自由

以及

类型级别的自由变成术语级别的约束

现在，让我们看看foo函数的第一条语句：

• 类型级别的约束..*

所以在类型签名上加一个约束

foo :: (Num a) => a -> a

• 成为术语级别的自由 * 使我们能够自由或灵活地编写所有这些内容

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

通过使用任何其他类型类等约束a也可以观察到同样的情况
那么现在这个类型的签名是什么：foo :: (Num a) => a -> a转换为：

∃a , st a -> a, ∀a ∈ Num

这被称为存在量化，它翻译为 there existsa的一些示例，当函数输入a类型的东西时，返回相同类型的东西，这些示例都属于Numbers集合。
因此，我们可以看到添加了一个约束（a应该属于Numbers集合），释放了术语级别，使其具有多个可能的实现。
现在来看看第二个语句，也就是实际解释forall的语句：

• 类型级别的自由变成术语级别的约束 *

现在让我们在类型级别释放函数：

foo :: forall a. a -> a

现在，这转化为：

∀a , a -> a

这意味着该类型签名的实现应当使得它对于所有环境都是a -> a。
所以现在这开始限制我们在术语层面上。我们不能再写

foo 5 = 7

因为如果我们将a作为Bool放置，此实现将无法满足。a可以是Char、[Char]或自定义数据类型。在所有情况下，它都应返回类似类型的内容。这种类型级别的自由性称为“通用量化”，唯一能够满足此要求的函数是

foo a = a

通常称为identity函数
因此，forall是类型级别的liberty，其实际用途是将术语级别的constrain应用于特定实现。

这个关键字有不同用法的原因是，它实际上至少在两种不同类型的系统扩展中使用：高级类型和存在式。
也许最好是分别阅读和理解这两件事，而不是试图解释为什么'forall'在这两件事中同时是一个合适的语法位。

存在主义是怎样的存在主义？

对于存在-量化，data定义中的forall s意味着，包含的值可以是任何合适的类型，而不是它必须是所有合适的类型。--yachiru's answer
关于为什么data定义中的forall同构于(exists a. a)（伪Haskell）的解释可以在维基百科的“Haskell/Existentially quantified types”中找到。
以下是简要的逐字摘要：

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

当模式匹配/解构MkT x时，x的类型是什么？

foo (MkT x) = ... -- -- what is the type of x?

x可以是任何类型（如forall中所述），因此其类型为：

x :: exists a. a -- (pseudo-Haskell)

因此，以下是同构的：

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

为了所有人就是为了所有人

我对这一切的简单解释是，“forall实际上意味着'for all'”。要做的一个重要区别是forall对定义和函数应用程序的影响。
forall表示值或函数的定义必须是多态的。
如果要定义的东西是多态的value，那么这意味着该值必须对所有合适的a有效，这是非常严格的。
如果被定义的是一个多态的函数，那么它意味着这个函数必须对所有合适的a都有效，这并不是很严格，因为仅仅因为这个函数是多态的并不意味着被应用的参数必须是多态的。则相反地，任何合适的a都可以应用到该函数。但是，参数的类型在函数定义中只能选择一次。
如果一个forall在函数参数的类型内部（即一个Rank2Type），则意味着applied参数必须是真正多态的，与forall的思想一致，意味着definition是多态的。在这种情况下，参数的类型可以在函数定义（"and is chosen by the implementation of the function", as pointed out by Norman）中选择多次。
因此，存在data定义允许any**a的原因是因为数据构造函数是一个多态函数：

MkT :: forall a. a -> T

市场类型：：a -> *
这意味着任何a都可以应用于该函数，与多态值相反：

valueT :: forall a. [a]

值类型T：：a
这意味着valueT的定义必须是多态的，在这种情况下，valueT可以定义为所有类型的空列表[]。

[] :: [t]

差异数量
尽管forall的含义在ExistentialQuantification和RankNType中是一致的，但存在性还是有区别的，因为data构造函数可以用于模式匹配。
当模式匹配时，每个模式匹配为每个存在类型变量引入一个新的、不同的类型。这些类型不能与任何其他类型统一，也不能脱离模式匹配的范围。