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东西...
我倾向于选择清晰，无行话的英语，而不是学术环境中正常的语言。 我尝试阅读的大部分解释（我可以通过搜索引擎找到的解释）都有这些问题：
runST ， foo和bar ）。 所以...
谈到实际问题。 任何人都可以用清晰，简单的英语完全解释forall关键字（或者，如果它存在的话，指出我错过的那种明确的解释），并不认为我是一个沉浸在行话中的数学家？
编辑添加：
下面有两个更高质量的答案，但不幸的是，我只能选择一个最好的答案。 诺曼的回答很详细的和有用的，解释的方式，表现出一定的理论基础的东西forall ，并在同一时间向我展示了一些它的实际影响。 yairchu的回答覆盖了其他人没有提到的领域（范围类型变量），并用代码和GHCi会话说明了所有的概念。 我可以选择两者都是最好的。 不幸的是，我不能，并且仔细查看两个答案后，我已经决定，由于说明性代码和附加说明，yairchu略微偏离了诺曼的范围。 然而，这有点不公平，因为我真的需要两个答案来理解这一点，即当我在类型签名中看到它时， 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关键字有三种不同的常见用途（或者至少看起来如此），并且每种都有它自己的Haskell扩展： ScopedTypeVariables ， RankNTypes / Rank2Types ， ExistentialQuantification Rank2Types 。
上面的代码没有得到任何启用的语法错误，但只有启用了ScopedTypeVariables类型检查。
作用域类型变量：
作用域类型变量有助于为where子句中的代码指定类型。 它使b在val :: b同一个作为b在foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b 。
一个令人困惑的一点：你可能会听到，当你忽略forall从类型它实际上仍隐含有。 （来自Norman的回答：“通常这些语言忽略了多态类型的所有内容”）。 这种说法是正确的， 但它指的是forall的其他用途，而不是ScopedTypeVariables用法。
排名-N-类型：
让我们从mayb :: b -> (a -> b) -> Maybe a -> b等同于mayb :: forall a b. 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 -> fx) -> (a, b) -> (fa, fb) 。 为了明白为什么，让我们试着对它进行编码：
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)
因此，不是所有x都可以使用的liftTup ，它的功能就是它。
存在量化：
我们来举个例子：
-- 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类型有什么不同？
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 s。 例如：
ghci> length ([] :: forall a. [a])
0
一个空列表可以用作任何类型的列表。
因此，与存在主义-定量， forall S IN data的定义是指，包含值可以是任何合适的类型，而不是它必须是适合所有类型的。
任何人都可以用清晰，简单的英文完整地解释forall关键字吗？
不， （也许唐斯图尔特可以。）
这里有一个简单，明确的解释或障碍forall ：
这是一个量词。 你有一个至少有一个小逻辑（谓词演算）已经看到了一个普遍的或存在的量词。 如果你从来没有见过谓词演算或不舒服的量词（我已经看到了在博士资格考试谁是不舒服的学生），那么对你来说，有没有简单的解释forall 。
这是一个类型量词。 如果你还没有看到系统F，并得到一些练习写多态类型，你会发现forall混乱。 哈斯克尔或ML经验是不够的，因为通常这些语言省略forall从多态类型。 （在我看来，这是一个语言设计错误。）
在Haskell特别forall在我发现混淆的方式使用。 （我不是一个类型理论家，但是我的工作让我接触到了很多类型理论，而且我对它很满意。）对于我来说，混淆的主要来源是forall用于编码类型我自己宁愿用exists写。 这是通过涉及量词和箭头的棘手的同构类型来证明的，每次我想了解它时，我都必须查找并自己找出同构。
如果你不舒服的同构型的想法，或者如果你没有任何实践思考型的同构，这种使用forall将会阻碍你。
虽然forall的一般概念总是相同的（绑定引入一个类型变量），但不同用途的细节可能会有很大差异。 非正式英语不是解释变化的很好工具。 要真正理解发生了什么，你需要一些数学。 在这种情况下，相关数学可以在本杰明皮尔斯的介绍性文本类型和编程语言中找到，这是一本很好的书。
至于你的具体例子，
runST应该让你的头部受伤。 更高等级的类型（箭头左侧）很少在野外找到。 我鼓励你阅读引入runST的论文：“懒惰功能状态线程”。 这是一篇非常好的论文，它会给你一个更好的直觉，特别是对于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关键字的完整解释需要数学，并且只能由研究数学的人理解。 没有数学，即使是部分解释也很难理解。 但也许我的部分，非数学解释有一点帮助。 在runST上阅读Launchbury和Peyton Jones！
附录： “左上方”，“下方”，“左侧”的术语。 这些与写入类型的文本方式以及与抽象语法树有关的所有内容无关。 在抽象语法中，一个forall采用一个类型变量的名称，然后在函数的“之下”有一个完整类型。 箭头有两种类型（参数和结果类型）并形成一个新类型（函数类型）。 参数类型是“在箭头的左侧”; 它是抽象语法树中箭头的左侧子元素。
例子：
在所有的forall a . [a] -> [a] forall a . [a] -> [a] ，所有人都在箭头之上; 箭头的左边是[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'只记得一件事： 它将类型绑定到某个范围 。 一旦你明白了，一切都相当简单。 它在类型层面上相当于'lambda'（或'let'的一种形式） - 诺曼拉姆齐使用“左”/“上”的概念在他的出色答案中传达了同样的范围概念。
'forall'的大多数用途都非常简单，您可以在GHC用户手册S7.8中找到它们，特别是嵌套形式的'forall'上的优秀S7.8.5。
在Haskell中，当类型被普遍量化时，我们通常会忽略类型的绑定，如下所示：
length :: forall a. [a] -> Int
相当于：
length :: [a] -> Int
而已。
由于您现在可以将类型变量绑定到某个作用域，所以您可以具有除顶层以外的作用域（“通用量化”），就像您的第一个示例，其中类型变量仅在数据结构中可见。 这允许隐藏类型（“存在类型”）。 或者我们可以任意绑定绑定（“排名N类型”）。
要深入了解类型系统，您需要学习一些术语。 这就是计算机科学的本质。 然而，像上面这样简单的用法应该能够直观地通过与价值层面上的'let'类比来掌握。 一个很好的介绍是Launchbury和Peyton Jones。
链接地址: http://www.djcxy.com/p/5669.html