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的东西…

我倾向于使用清晰、无专业术语的英语，而不是学术环境中常见的语言。我试图阅读的大部分解释(我可以通过搜索引擎找到的)都有这些问题:

  1. 他们是不完整的。它们解释了这个关键字使用的一部分(如“存在类型”)，这让我感到高兴，直到我读到以完全不同的方式使用它的代码(如上面的runST， foo和bar)。
  2. 它们密密麻麻地塞满了假设，即我已经阅读了本周最流行的离散数学、范畴理论或抽象代数的任何分支的最新研究成果。(如果我从来没有读过“咨询论文无论实现细节”这句话，那就为时过早了。)
  3. 它们的编写方式经常把简单的概念变成扭曲和断裂的语法和语义。

所以…

回到真正的问题上来。有人能完全解释forall关键字清楚，简单的英语(或者，如果它存在的地方，指向这样一个明确的解释，我错过了)，不假设我是一个数学家沉浸在行话?

编辑补充:

下面有两个高质量的答案，但不幸的是，我只能选择一个最好的。诺曼的回答是详细而有用的，以一种显示forall的一些理论基础的方式解释事情，同时向我展示了它的一些实际含义。yairchu的回答涵盖了一个没有人提到的领域(作用域类型变量)，并用代码和GHCi会话说明了所有的概念。如果有可能两者都选得最好，我会选。不幸的是，我不能，在仔细查看了两个答案后，我认为yairchu的答案略优于Norman的答案，因为其中有说明性代码和附带的解释。然而，这有点不公平，因为我真的需要两个答案来理解这一点，以至于当我在类型签名中看到forall时，它不会让我有一种微弱的恐惧感。

56081 次浏览
小开

有人能用清楚、简单的英语解释forall关键字吗?

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

下面是一个简单明了的解释或forall的障碍:

  • 它是一个量词。你至少要有一点逻辑(谓词演算)才能看到一个全称量词或存在量词。如果你从未见过谓词演算或对量词不熟悉(我在博士资格考试中见过不熟悉的学生)，那么对你来说，forall没有简单的解释。

  • 它是一个类型量词。如果你没有看过System F，并且有过一些编写多态类型的练习，你会发现forall令人困惑。有Haskell或ML经验是不够的，因为通常这些语言会从多态类型中省略forall。(在我看来，这是语言设计上的错误。)

  • 特别是在Haskell中，forall的使用方式让我感到困惑。(我不是类型理论家，但我的工作使我接触到类型理论的很多，而且我对它很满意。)对我来说，困惑的主要来源是forall用于编码我自己更喜欢用exists编写的类型。它是由一些复杂的类型同构来证明的，包括量词和箭头，每次我想理解它，我都得自己查资料，找出同构。

    如果你不适应类型同构的概念，或者如果你没有任何思考类型同构的练习，forall的使用将会阻碍你

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

至于你的具体例子，

  • runST should make your head hurt。更高等级的类型(箭头左边的所有类型)在野外很少发现。我鼓励你阅读介绍runST的论文:"Lazy Functional State Threads"。这是一篇非常好的论文，它会让你对runST类型有更好的直觉，尤其是对更高级别的类型。解释花了好几页，写得很好，我就不把它浓缩在这里了。

  • < p >考虑

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

    如果我调用bar，我可以简单地选择任何我喜欢的类型a，并且我可以将一个函数从类型a传递给类型a。例如，我可以传递函数(+1)或函数reverse。你可以认为forall是在说“我现在可以选择类型了”。(选择类型的专业术语是实例化。)

    调用foo的限制要严格得多:foo foo3的实参是一个多态函数。对于这种类型，唯一可以传递给foo的函数是id或者总是发散或出错的函数，比如undefined。原因是在foo中，forall在箭头的左边，所以作为foo的调用者，我不能选择a是什么，而是foo的foo4可以选择a是什么。因为forall在箭头的左边，而不是像foo2那样在箭头的上面，所以实例化发生在函数体中，而不是在调用点

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

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

例子:

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

  • < p >

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

    括号中的类型被称为“箭头左边的a forall”。(我在一个优化器中使用这样的类型)

小开

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

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

所以，如果这没有帮助，或者如果你只是不喜欢符号逻辑，从更函数式编程的角度来看，你可以认为类型变量只是函数的(隐式)类型参数。在这种意义上，接受类型参数的函数通常使用大写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的类型形参。考虑一下如果你有这样的东西:

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

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

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

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 a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b中的b相同。

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

Rank-N-Types:

首先，当启用ScopedTypeVariables时，mayb :: b -> (a -> b) -> Maybe a -> b等价于mayb :: forall a b. b -> (a -> b) -> Maybe a -> b， 除了。

这意味着它适用于每个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

这和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意味着你的表达式必须符合所有可能的__abc1。例如:

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

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

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

小开

我最初的回答是:

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

正如诺曼所指出的那样，要用清楚明了的英语解释是非常困难的 类型理论中的一个专业术语。

关于'forall'只有一件事需要记住:它绑定类型 一些范围> < /强。一旦你理解了这一点，一切都相当简单。它是 在类型层面上相当于“lambda”(或“let”的一种形式)——诺曼·拉姆齐 在his中使用“左”/“上方”的概念来传达相同的作用域概念 优秀的答案< / > . < / p > 'forall'的大多数用法都很简单，你可以在the GHC用户手册，S7.8。，特别是嵌套上的出色的S7.8.5

. 'forall'的形式 在Haskell中，当类型为时，我们通常不使用类型绑定符 通用量化，像这样:

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

等价于:

length :: [a] -> Int

就是这样。

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

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

小开

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

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

通用量化

普遍量化类型是形式为forall a. f a的类型。该类型的值可以被认为是一个函数，它接受类型 a作为参数，并返回类型为f a的价值。除了在Haskell中，这些类型参数是由类型系统隐式传递的。这个“function"无论它接收到哪种类型，都必须给你相同的值，所以值是多态。

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

或者forall a. a -> a类型。此类函数的调用者提供类型a和类型a的值。然后该实现必须返回相同类型的a值。只有一种可能的实现。它必须返回与给定值相同的值。

存在量化

如果Haskell支持这种表示法，存在量化类型将具有exists a. f a的形式。该类型的值可以被认为是一对(或“product”)，由类型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支持这种符号的话。

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. ST s a的实参，该实参必须以某种方式生成a。更重要的是，它必须能够产生一个类型为a的值，无论runST的实现决定将什么类型作为s。

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

好吧，那又怎样?这样做的好处是对runST的调用者施加了约束，因为类型a根本不能涉及类型s，因为你不知道s将是什么类型。例如，不能将类型为ST s [s]的值传递给它。在实践中，这意味着runST的实现可以知道任何涉及s类型的值对于它自己的实现来说都是局部的，因此它可以自由地做一些否则不允许做的事情，比如在适当的地方改变它们。该类型保证该突变是runST的局部实现。

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

小开

存在主义是如何存在的?

对于存在量化，__abc0在data定义中表示 即包含可以的值是任何的合适类型，而不是 它必须是所有合适的类型。 ——yachiru的回答 < / p >

关于为什么data定义中的forall与(exists a. a)同构(pseudo-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真的意味着‘对于所有人’”。 要做的一个重要区别是forall对定义和应用程序函数的影响

forall表示值或函数的定义必须是多态的。

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

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

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

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

MkT :: forall a. a -> T

kind of MkT:: a -> *

这意味着任何a都可以应用于该函数。与之相反的是，多态的价值:

valueT :: forall a. [a]

类型valueT:: a

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

[] :: [t]

差异

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

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

小开

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

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

但在你理解之前，我想引导你去看Runar Bjarnason的一个非常平易近人的演讲，题为“约束解放，自由约束”。这次演讲充满了来自现实世界的用例以及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 :: (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的东西时返回相同类型的东西，这些实例都属于数字集。

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

现在来看第二个语句，它实际上包含了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用于特定的实现。


提交答案