有谁能用清楚明了的英语完全解释forall关键字吗?

不。(嗯，也许唐·斯图尔特(Don Stewart)可以。)

以下是一个简单明了的解释或所有解释的障碍:

It's a quantifier. You have a to have at least a little logic (predicate calculus) to have seen a universal or existential quantifier. If you've never seen predicate calculus or are not comfortable with quantifiers (and I have seen students during PhD qualifying exams who are not comfortable), then for you, there's no easy explanation of forall. It's a type quantifier. If you haven't seen System F and gotten some practice writing polymorphic types, you're going to find forall confusing. Experience with Haskell or ML is not enough, because normally these languages omit the forall from polymorphic types. (In my mind, this is a language-design mistake.) In Haskell in particular, forall is used in ways that I find confusing. (I'm not a type theorist, but my work brings me in contact with a lot of type theory, and I'm quite comfortable with it.) For me, the main source of confusion is that forall is used to encode a type that I myself would prefer to write with exists. It's justified by a tricky bit of type isomorphism involving quantifiers and arrows, and every time I want to understand it, I have to look things up and work out the isomorphism myself. If you are not comfortable with the idea of type isomorphism, or if you don't have any practice thinking about type isomorphisms, this use of forall is going to stymie you. While the general concept of forall is always the same (binding to introduce a type variable), the details of different uses can vary significantly. Informal English is not a very good tool for explaining the variations. To really understand what's going on, you need some mathematics. In this case the relevant mathematics can be found in Benjamin Pierce's introductory text Types and Programming Languages, which is a very good book.

至于你的具体例子，

runST should make your head hurt. Higher-rank types (forall to the left of an arrow) are rarely found in the wild. I encourage you to read the paper that introduced runST: "Lazy Functional State Threads". This is a really good paper, and it will give you a much better intuition for the type of runST in particular and for higher-rank types in general. The explanation take several pages, it's very well done, and I'm not going to try to condense it here. Consider foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool)) If I call bar, I can simply pick any type a that I like, and I can pass it a function from type a to type a. For example, I can pass the function (+1) or the function reverse. You can think of the forall as saying "I get to pick the type now". (The technical word for picking the type is instantiating.) The restrictions on calling foo are much more stringent: the argument to foo must be a polymorphic function. With that type, the only functions I can pass to foo are id or a function that always diverges or errors, like undefined. The reason is that with foo, the forall is to the left of the arrow, so as the caller of foo I don't get to pick what a is—rather it's the implementation of foo that gets to pick what a is. Because forall is to the left of the arrow, rather than above the arrow as in bar, the instantiation takes place in the body of the function rather than at the call site.

摘要:forall关键字的完整解释需要数学，并且只有研究过数学的人才能理解。如果没有数学，即使是部分的解释也很难理解。但也许我的片面的、非数学的解释有一点帮助。去runST上看Launchbury和Peyton Jones吧!

---

补充:行话“在上面”，“在下面”，“在左边”。这些与编写类型的文本方式无关，而是与抽象语法树有关。在抽象语法中，forall接受类型变量的名称，然后在forall“下面”有一个完整类型。箭头有两种类型(参数和结果类型)，并形成一个新类型(函数类型)。参数类型是“箭头左边”;它是抽象语法树中箭头的左子元素。

例子:

In all总之;[a] -> [a]， forall在箭头上方;箭头左边的是[a]。 在 对于所有n f x。(forall e x。n e x -> f ->事实x f) -> Block n e x -> f ->事实x f 括号中的类型被称为“箭头左边的a forall”。(我在我正在工作的优化器中使用这样的类型。)

它们密密麻麻地塞满了假设，即我已经阅读了本周最流行的离散数学、范畴理论或抽象代数的任何分支的最新研究成果。(如果我再也没有读过“关于实施细节，无论如何，请查阅报纸”这句话，那就为时过早了。)

那么简单的一阶逻辑呢?Forall很明显是指普遍量化，在这种情况下，术语存在主义也更有意义，尽管如果有一个存在关键字就不那么尴尬了。量化是普遍的还是存在的取决于量词相对于变量在函数箭头的哪一边使用的位置，这有点令人困惑。

因此，如果这没有帮助，或者如果您只是不喜欢符号逻辑，从更函数式编程的角度来看，您可以将类型变量视为函数的(隐式)类型参数。在这种意义上，接受类型参数的函数通常使用大写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 = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

注意，作为参数赋给bar的函数类型取决于bar的类型形参。考虑一下如果你有这样的东西:

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绑定的类型变量仅在量化表达式的作用域内。

---

Post scriptum:也许您会想——既然我们正在考虑函数接受类型参数，为什么我们不能对这些参数做一些更有趣的事情，而不是将它们放入类型签名中呢?答案是我们可以!

将类型变量与标签放在一起并返回新类型的函数是类型构造函数，你可以这样写:

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'同时在这两件事上都是合适的语法。

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

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子句中为代码指定类型。它使得val:: b中的b与foob:: forall中的b相同。(b -> b) -> b -> (a -> b) ->也许是a -> b。

令人困惑的一点是:当你从一个类型中省略forall时，它实际上仍然隐式存在。(来自Norman的回答:“通常这些语言会从多态类型中省略forall”)。这个声明是正确的，但它指的是forall的其他用法，而不是ScopedTypeVariables的用法。

Rank-N-Types:

让我们从mayb:: b -> (a -> b) ->也许a -> b等价于mayb:: forall ab b -> (a -> b) ->也许a -> b，除非ScopedTypeVariables被启用。

这意味着它对所有a和b都成立。

假设你想做这样的事情。

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

这个电梯一定是什么类型的?它是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

这和Rank-N-Types有什么不同?

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

对于Rank-N-Types, forall a意味着你的表达式必须适合所有可能的。例如:

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

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

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

我最初的回答是:

有谁能用清楚明了的英语完全解释forall关键字吗

正如诺曼所指出的，要给出一个清晰明了的英语解释是非常困难的 类型理论中的一个专业术语。我们都在努力。

关于“forall”只需要记住一件事:它将类型绑定到 一些范围。一旦你理解了这一点，一切都相当简单。它是 在类型层面上相当于“lambda”(或“let”的一种形式)——诺曼·拉姆齐 使用“左边”/“上面”的概念来传达他的范围的相同概念 优秀的答案。

'forall'的大多数用法都很简单，你可以在词典中找到它们的介绍 GHC用户手册，S7.8。特别是出色的S7.8.5上的嵌套 forall的形式。

在Haskell中，当类型为时，我们通常不使用类型绑定器 被普遍量化的，像这样:

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

等价于:

length :: [a] -> Int

就是这样。

既然现在可以将类型变量绑定到某个作用域，那么还可以拥有其他作用域 而不是顶层(“普遍量化”)，就像你的第一个例子， 其中类型变量仅在数据结构中可见。这允许 对于隐藏类型(“存在类型”)。或者我们可以用任意 绑定嵌套(“排序N类型”)。

要深入理解类型系统，您需要学习一些术语。这是 计算机科学的本质。然而，简单的使用，如上述，应该是 可以通过在价值层面上类比“let”来直观地理解。一个 很好的介绍是Launchbury和Peyton Jones。

这里有一个简单明了的解释，你可能已经熟悉了。

forall关键字在Haskell中实际上只以一种方式使用。当你看到它的时候，它的意思总是一样的。

通用量化

通用量化类型是forall形式的类型。该类型的值可以被认为是一个以类型为参数并返回类型为值的函数。不同的是，在Haskell中，这些类型参数是由类型系统隐式传递的。这个“函数”必须给你相同的值，无论它接收到哪种类型，所以这个值是多态的。

例如，考虑所有a. [a]的类型。该类型的值接受另一种类型A，并返回相同类型A的元素列表。当然，只有一种可能的实现。它会给你一个空列表因为a可以是任何类型。空列表是其元素类型中唯一的多态列表值(因为它没有元素)。

a.这样一个函数的调用者提供了类型a和类型a的值。然后实现必须返回相同类型a的值。再次只有一个可能的实现。它必须返回与给定值相同的值。

存在量化

如果Haskell支持这种表示法，存在量化类型的形式为exists a. f a。该类型的值可以被认为是由类型A和类型f A的值组成的一对(或“产品”)。

例如，如果你有一个类型为exists . [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支持这个符号的话。

runST和朋友

既然如此，它们有什么不同呢?

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的实参，这肯定会以某种方式产生a。更重要的是，它必须能够产生一个类型为a的值，不管runST的实现决定把什么类型作为s。

所以实际上runST函数是在告诉你:“只要我可以选择类型s，你就可以选择类型a。”

OK, so what? The benefit is that this puts a constraint on the caller of runST in that the type a cannot involve the type s at all, since you don't know what type s is going to be. You can't pass it a value of type ST s [s], for example. What that means in practice is that the implementation of runST can know that any value involving the type s is local to its own implementation, so it's free to do things it otherwise wouldn't be allowed to, like mutate them in place. The type guarantees that the mutation is local to the implementation of runST.

runST类型是2级多态类型的一个例子，因为它的参数类型包含forall量词。上面的foo类型也是秩2。一个普通的多态类型，比如bar，是rank-1，但是如果参数类型被要求是多态的，它就变成了rank-2，有它们自己的forall量词。如果一个函数接受2级参数，那么它的类型就是3级，依此类推。一般来说，接受秩n的多态参数的类型具有秩n + 1。

存在主义是如何存在的?

对于存在量化，数据定义中的foralls意味着 即，所包含的值可以是任何合适的类型，而不是 它必须是所有合适的类型。 ——yachiru的回答

为什么forall在数据定义是同构的(存在a. a)(伪Haskell)可以在wikibooks的“Haskell/存在量化类型”中找到解释。

以下是简要的逐字摘要:

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”实际上意味着“为所有人”。 一个重要的区别是forall对定义和函数应用程序的影响。

forall意味着值或函数的定义必须是多态的。

如果被定义的东西是一个多态值，那么它意味着该值必须对所有合适的a有效，这是非常严格的。

如果被定义的是一个多态函数，那么它意味着这个函数必须对所有合适的a都有效，这并不是限制性的，因为仅仅因为函数是多态的并不意味着应用的参数必须是多态的。也就是说，如果函数对所有a都有效，那么反过来，任何合适的a都可以应用于该函数。但是，在函数定义中，参数的类型只能选择一次。

如果forall在函数参数的类型中(即Rank2Type)，那么它意味着应用的参数必须是真正多态的，与forall的思想一致，意味着定义是多态的。在这种情况下，在函数定义中可以多次选择形参的类型(正如Norman所指出的，“并且由函数的实现选择”)。

因此，存在数据定义允许任何a的原因是因为数据构造函数是一个多态函数:

MkT :: forall a. a -> T

kind of MkT:: a -> *

这意味着任何a都可以作用于这个函数。与之相反的是，例如，一个多态值:

valueT :: forall a. [a]

类型值et:: a

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

[] :: [t]

差异

尽管在ExistentialQuantification和RankNType中forall的含义是一致的，但existentials有区别，因为数据构造函数可以用于模式匹配。如ghc用户指南中所述:

当进行模式匹配时，每个模式匹配都会为每个存在类型变量引入一个新的、不同的类型。这些类型不能与任何其他类型统一，也不能逃脱模式匹配的范围。

有谁能用清楚明了的英语完全解释forall关键字(或者，如果它存在的话，指出一个我错过的如此清晰的解释)，而不假设我是一个沉浸在行话中的数学家吗?

我将试着解释forall在Haskell及其类型系统上下文中的含义和应用。

但在你们理解之前，我想先给你们介绍一下Runar Bjarnason的一篇非常通俗易懂的演讲，题目是“约束解放，自由约束”。演讲中充满了来自现实世界的用例以及Scala中的示例来支持这一说法，尽管它并没有全部提到。我将试着在下面解释所有的观点。

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

理解并相信这句话对接下来的解释非常重要，所以我强烈建议你看一看我的演讲(至少是部分)。

下面是一个非常常见的例子，它展示了Haskell类型系统的表达能力:

Foo:: a -> a

据说，给定这个类型签名，只有一个函数可以满足这个类型，那就是恒等函数，或者更通俗地说是id函数。

在我学习Haskell的开始阶段，我总是想知道下面的函数:

foo 5 = 6

foo True = False

它们都满足上面的类型签名，那么为什么Haskell的人声称它是id单独满足类型签名?

这是因为在类型签名中隐藏了一个隐式的forall。实际的类型是:

id :: forall a. a -> a

所以，现在让我们回到这句话:约束解放，自由约束

将其转换为类型系统，该语句变成:

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

and

类型层面的自由，变成了术语层面的约束

---

现在，让我们看看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

这就是所谓的存在量化，也就是说存在一些实例，在这些实例中，一个函数在被输入类型为a的东西时返回相同类型的东西，这些实例都属于数字集合。

因此，我们可以看到添加一个约束(a应该属于数字集)，解放了术语级别，使其具有多种可能的实现。

---

现在来看第二种说法，它实际上解释了所有的事情:

类型层面的自由，变成了术语层面的约束

现在让我们在类型级别上解放函数:

foo :: forall a. a -> a

这句话的意思是:

∀a , a -> a

这意味着这种类型签名的实现应该在所有情况下都是-> a。

现在这开始在期限层面约束我们了。 我们不能再写了

foo 5 = 7

因为如果我们把a作为Bool类型，这个实现就不满足了。a可以是Char或[Char]或自定义数据类型。在任何情况下，它都应该返回类似类型的东西。这种类型层面上的自由就是所谓的普遍量化，而唯一能满足这一点的函数是

foo a = a

哪个通常被称为恒等函数

---

因此，forall是类型级别的自由，其实际目的是将术语级别约束到特定的实现。