Haskell / GHC中的`forall`关键字是做什么的?

我开始了解如何在所谓的“存在types”中使用forall关键字:

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

然而,这只是一个子集,因为它是如何使用的,而我根本无法把它用在这样的事情上:

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

或者解释为什么这些不同:

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

或者整个RankNTypes东西…

我倾向于select清晰,不含行话的英语,而不是学术环境中正常的语言。 我试图阅读的大部分解释(我可以通过search引擎find的)有这些问题:

  1. 他们不完整。 他们解释了使用这个关键字(比如“存在types”)的一部分,这让我感觉很开心,直到我读完以不同的方式使用它的代码(比如runSTfoobar )。
  2. 他们密集的假设,我已阅读离散math的任何分支,类别理论或抽象代数本周stream行的最新。 (如果我再也不读“实施细节咨询文件”,那就太快了。)
  3. 他们的写作方式经常会把简单的概念变成扭曲和破碎的语法和语义。

所以…

谈到实际的问题。 任何人都可以用清晰,简单的英语(或者,如果存在的话,指出我错过的一个明确的解释)完全解释forall关键字,并不假定我是一个沉浸在行话中的math家?


编辑添加:

下面有两个更高质量的答案,但不幸的是,我只能select一个最好的答案。 诺曼的回答是详细而有用的,以某种方式解释事情,显示了一些理论的基础,同时也给我一些实际的含义。 yairchu的答案涵盖了一个没有人提到的区域(范围typesvariables),并用代码和GHCi会话说明了所有的概念。 我可以select两者都是最好的。 不幸的是,我不能,而且仔细查看两个答案之后,我已经决定,由于说明性的代码和附加的解释,Yairchu略微偏离了Norman的。 但是,这有点不公平,因为我真的需要两个答案来理解这个问题,即当我在types签名中看到这个问题时, 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关键字有三种不同的常见用法(至less看起来如此),每种都有自己的Haskell扩展: ScopedTypeVariablesRankNTypes / Rank2TypesExistentialQuantification

上面的代码没有得到任何启用的语法错误,但只有启用了ScopedTypeVariablestypes检查。

作用域typesvariables:

作用域typesvariables有助于为where子句中的代码指定types。 它使val :: b中的bfoob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b

一个令人困惑的问题是 :你可能会听到,当你从一个types中忽略所有的实际时,它实际上仍然隐含在那里。 ( 从诺曼的回答:“通常这些语言省略多态types的所有 )”。 这个说法是正确的, 它指的是其他用途,而不是ScopedTypeVariables用法。

排名-N-types:

我们从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被启用。

这意味着它适用于每个ab

假设你想要做这样的事情。

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

什么是这种liftTup的types? 它是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推断这个元组必须包含两个相同的types呢?让我们告诉它它们不一定是”

 -- test.hs liftTup :: (x -> fx) -> (a, b) -> (fa, fb) 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 :: bliftFunc一个x 。 我们真的希望我们的函数得到一个接受任何可能的x

 {-# LANGUAGE RankNTypes #-} liftTup :: (forall x. x -> fx) -> (a, b) -> (fa, fb) liftTup liftFunc (t, v) = (liftFunc t, liftFunc v) 

所以,不是所有的x都可以使用的liftTup ,它的function就是这样。

存在量化:

我们用一个例子:

 -- 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-Ntypes有什么不同?

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

有了Rank-N-Types,所有forall a意思是你的expression必须适合所有可能a s。 例如:

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

一个空列表可以用作任何types的列表。

因此,在存在量化的情况下, data定义中的全部意思是,所包含的值可以任何适合的types,而不是它必须所有适合的types。

任何人都可以用清晰,简单的英文完整地解释关键字吗?

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

以下是一个简单,明确的解释或forall的障碍:

  • 这是一个量词。 你有一个至less有一个小逻辑(谓词演算)已经看到了一个普遍的或存在的量词。 如果你从来没有见过谓语演算,或者对量词不熟悉(而且我在博士资格考试期间看到学生不舒服),那么对你来说,没有一个简单的解释。

  • 这是一个types量词。 如果你没有看到系统F,并得到一些练习写多态types,你会发现所有的混淆。 与Haskell或ML的经验是不够的,因为通常这些语言省略多态types的所有。 (在我看来,这是一个语言devise的错误。)

  • 特别是在Haskell中,使用方式让我感到困惑。 (我不是一个types理论家,但是我的工作让我接触到了很多types理论,而且我对它很满意。)对我来说,混淆的主要来源是用于编码一个types我本人宁愿写与exists 。 这是通过涉及量词和箭的types同构的棘手的理由,每当我想了解它,我不得不查找的东西,并找出自己的同构。

    如果你不习惯types同构的概念,或者如果你没有任何关于types同构的实践,这种使用将会阻碍你。

  • 虽然forall的一般概念总是相同的(绑定引入一个typesvariables),不同用途的细节可能会有很大的不同。 非正式的英语不是一个很好的解释变化的工具。 要真正理解正在发生的事情,你需要一些math。 在这种情况下,相关的math可以在本杰明·皮尔斯(Benjamin Pierce)的介绍性文本types和编程语言Types and Programming Languages)中find ,这是一本很好的书。

至于你的具体例子,

  • runST 应该让你的头受伤。 更高级的types(箭头左侧)很less在野外find。 我鼓励你阅读引入runST的论文: “懒惰function状态线程” 。 这是一个非常好的论文,它会给你一个更好的直觉,尤其是对于runST的types,对于更高级别的types。 这个解释需要几页,这是很好的,我不打算在这里浓缩它。

  • 考虑

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

    如果我打电话给bar ,我可以简单地select任何我喜欢的types,我可以将它从typesa传递给typesa 。 例如,我可以通过function(+1)或functionreverse 。 你可以把所有的想法说成“我现在select这个types”。 (selecttypes的技术词是实例化的 。)

    调用foo的限制要严格得多: foo的参数必须是一个多态函数。 使用这种types,我可以传递给foo的唯一函数是id或者一个总是偏离或者错误的函数,就像undefined 。 原因在于fooforall在箭头的左边,所以作为foo的调用者,我不会去挑选什么,而是foo实现来挑选a是什么。 由于所有实例都在箭头的左侧,而不是在箭头的上方,所以实例化发生在函数的主体中,而不是在调用位置。

总结:对关键字的完整解释需要math,只有学过math的人才能理解。 即使是部分的解释,没有math也是难以理解的。 但也许我的部分,非math解释有一点帮助。 在runST上阅读Launchbury和Peyton Jones!


附录: “左上方”,“下方”,“左侧”的术语。 这些与写入types的文本方式以及与抽象语法树有关的一切无关。 在抽象的语法中,一个forall取一个typesvariables的名字,然后在函数的“之下”有一个完整的types。 箭头有两种types(参数和结果types)并形成一个新的types(函数types)。 参数types是“在箭头的左边” 它是抽象语法树中箭头的左边的孩子。

例子:

  • 在所有的forall a . [a] -> [a] forall a . [a] -> [a] ,所有的都在箭头之上; 箭头的左边是[a]

  •  forall nfex . (forall ex . nex -> f -> Fact xf) -> Block nex -> f -> Fact xf 

    括号中的types将被称为“箭头左侧”。 (我正在使用我正在优化的types。)

我原来的答案是:

任何人都可以用简单明了的英文完整地解释关键字

正如诺曼所指出的那样,很难从types理论中对技术术语给出明确,简单的英语解释。 我们都尝试。

关于'forall'只记得一件事: 它把types绑定到某个范围 。 一旦你明白了,一切都相当简单。 它在types层面上相当于“lambda”(或“let”forms) – Norman Ramsey用他的“左”/“上”的概念来传达这个相同的范围概念。

'forall'的大部分用法都非常简单,你可以在GHC用户手册S7.8中find它们,尤其是嵌套在'forall'上的S7.8.5 。

在Haskell中,当我们通常对数据types进行量化时,我们通常会忽略types的绑定,如下所示:

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

相当于:

 length :: [a] -> Int 

而已。

既然可以将typesvariables绑定到某个作用域,那么可以使用顶层以外的作用域(“ 通用量化 ”),就像第一个例子,其中typesvariables只在数据结构中可见。 这允许隐藏types(“ 存在types ”)。 或者我们可以任意绑定绑定(“排名Ntypes”)。

要深入了解types系统,您需要学习一些术语。 这就是计算机科学的本质。 但是,像上面这样简单的用法,应该能够通过与价值层面上的“让”类比来直观地掌握。 Launchbury和Peyton Jones是一个很好的介绍。

他们密集的假设,我已阅读离散math的任何分支,类别理论或抽象代数本周stream行的最新。 (如果我再也不读“实施细节咨询文件”,那就太快了。)

呃,简单的一阶逻辑呢? 对于普遍的量化来说 ,所有的东西都是非常清楚的,在这种情况下, 存在这个词也更有意义,但是如果存在一个关键词,那么它就不那么尴尬了。 量化是否具有普遍性或存在性取决于量词相对于在function箭头的哪一侧使用variables的位置的放置,并且这有点混乱。

所以,如果这没有帮助,或者如果你不喜欢符号逻辑,从更多的function编程angular度来看,你可以把typesvariables看作是函数的(隐式) types参数。 从这个意义上讲,types参数的函数传统上使用大写的lambdaexpression式出于任何原因,我将在这里写成/\

所以,考虑一下id函数:

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

我们可以将其重写为lambdaexpression式,将“types参数”移出types签名并添加内联types注释:

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

这与const所做的相同:

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

所以你的barfunction可能是这样的:

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

请注意,作为参数给bar的函数的types取决于bar的types参数。 考虑如果你有这样的事情,而不是:

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

这里bar2正在把这个函数应用到Chartypes的东西上,所以给bar2任何types参数都会导致types错误。

另一方面,下面是foo样子:

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

bar不同的是, foo实际上并没有带任何types的参数! 它需要一个函数, 它自己接受一个types参数,然后将该函数应用于两种不同的types。

所以当你看到一个types签名的时候,可以把它看作是types签名lambdaexpression式 。 就像普通的lambda一样,函数的作用域尽可能地向右延伸,直到括起括号,就像正则lambda中绑定的variables一样,由forall绑定的typesvariables只在量化expression式的范围内。


Post scriptum :也许你可能会想知道 – 现在我们正在考虑采用types参数的函数,为什么我们不能用这些参数做一些更有趣的事情,而不是把它们放在types签名中呢? 答案是我们可以!

将typesvariables和标签放在一起并返回一个新types的函数是一个types构造函数 ,你可以这样写:

 Either = /\ab -> ... 

但是我们需要全新的符号,因为写这样一个types的方式,比如Either ab ,已经暗示了“将函数应用于这些参数”。

另一方面,一个types参数“模式匹配”的函数,为不同types返回不同的值,是一个types类方法 。 稍微扩展到我的/\上面的语法表明这样的事情:

 fmap = /\ fab -> case f of Maybe -> (\gx -> case x of Just y -> Just bgy Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b [] -> (\gx -> case x of (y:ys) -> gy : fmap [] abg ys [] -> [] b) :: (a -> b) -> [a] -> [b] 

就个人而言,我认为我更喜欢Haskell的实际语法…

“模式匹配”其types参数并返回任意现有types的函数是一个types族函数依赖关系 – 在前一种情况下,它甚至已经看起来很像函数定义。

用简单的话来说,这是一个快速和肮脏的解释,你可能已经熟悉了。

forall关键字实际上只在Haskell中以一种方式使用。 当你看到它时,它总是意味着同样的东西。

通用量化

一个普遍量化的types是一种forms的forall a. fa forall a. fa 。 该types的值可以认为是一个函数 ,它将一个types a作为其参数,并返回一个types为fa 。 除了在Haskell中,这些types参数是由types系统隐式传递的。 这个“函数”必须给你相同的值,不pipe它接收哪种types,所以这个值是多态的

例如,考虑typesforall a. [a] forall a. [a] 。 该types的值使用另一个typesa ,并返回相同typesa的元素列表。 当然,只有一个可能的实现。 它将不得不给你空的名单,因为可能是绝对的任何types。 空列表是唯一的元素types为多态的列表值(因为它没有元素)。

或者types为forall a. a -> a forall a. a -> a 。 这种函数的调用者提供了typesa和typesa的值。 然后实现必须返回相同typesaa 。 只有一个可能的实施再次。 它将不得不返回它给出的相同的价值。

存在量化

存在量化types将有formsexists a. fa exists a. fa ,如果Haskell支持这个表示法。 该types的值可以被认为是由typesa和typesfa的值组成的一 (或“产品”)。

例如,如果你有一个types的值exists a. [a] exists a. [a] ,你有一个types的元素列表。 它可以是任何types的,但即使你不知道它是什么,你可以做这样一个列表。 您可以反转它,也可以统计元素的数量,或者执行不依赖于元素types的其他列表操作。

好的,等一下。 为什么Haskell使用forall来表示如下的“存在”types?

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

这可能会令人困惑,但它确实描述了数据构造器 SBtypes

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

一旦构build,您可以将ShowBoxtypes的值视为由两件事组成。 这是一个typess和一个typess的值。 换句话说,这是一个存在量化types的价值。 ShowBox真的可以写成exists s. Show s => s exists s. Show s => s ,如果Haskell支持该表示法。

runST和朋友

鉴于这些,这些不同呢?

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

我们先拿bar 。 它采用typesa和函数a -> a ,并生成一个types(Char, Bool) 。 我们可以selectInt作为a并给它一个Int -> Inttypes的函数。 但是foo是不同的。 它要求foo实现能够将它想要的任何types传递给我们给它的函数。 所以我们合理的唯一的function就是id

现在我们应该能够解决runSTtypes的runST

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

所以runST必须能够产生一个typesa的值,而不pipe我们给出的typesa什么。 要做到这一点,它需要一个types为forall s. ST sa的论据forall s. ST sa 在引擎盖下面的forall s. ST sa是只是types的functionforall s. s -> (a, s) forall s. s -> (a, s) 。 那么这个函数必须能够产生一个types(a, s)的值,不piperunST的实现types决定给出什么types。

好的,那又怎么样? 好处是这对runST的调用者有一个约束,因为typesa根本不能包含typess 。 例如,您不能将它传递给ST s [s]types的值。 这在实践中意味着runST的实现可以自由地使用typess的值进行变异。 types系统保证这个变异对runST的实现是本地的。

runST的types是rank-2多态types的一个例子,因为它的参数types包含一个全量词。 上面的footypes也是等级2.一个普通的多态types,像bar ,是rank-1,但是如果参数的types需要是多态的,用它们自己的所有量词,它就变成了rank-2。 如果一个函数需要等级2的参数,那么它的types是等级3,依此类推。 一般来说,一个具有秩n + 1多态参数的types具有秩n + 1

这个关键字有不同用途的原因是,它至less在两种不同types的系统扩展中被使用:高级types和存在。

最好是单独阅读和理解这两件事情,而不是试图解释为什么“全部”是同时适合的语法。

存在主义是如何存在的?

通过存在量化, data定义中的全部意思是,所包含的值可以任何适当的types,而不是它必须所有适合的types。 – yachiru的回答

在wikibooks的“Haskell / Existentially quantified types”中可以find解释为什么data定义同构(exists a. a) a。a)(伪Haskell)的原因。

以下是简短的逐字摘要:

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

当模式匹配/解构MkT xMkT x的types是什么?

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

x可以是任何types(如所述),所以它的types是:

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

所以下面是同构的:

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

全部意味着全部

我对这一切的简单解释是:“所有的真正意义”都是“真正意义上的”。 要做的一个重要的区别是全部对定义和function应用的影响

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

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

如果被定义的东西是一个多态函数 ,那么它意味着该函数必须对所有合适的a有效,这不是限制性的,因为只是因为函数是多态的,并不意味着被应用的参数必须是多态的。 也就是说,如果该函数对所有a都有效,则相反,可以将任何合适的a 应用于该函数。 但是,参数的types只能在函数定义中select一次。

如果函数参数的types(即一个Rank2Type )的内部,那么它意味着应用参数必须是真正的多态,以符合所有方法定义是多态的想法。 在这种情况下,参数的types可以在函数定义中多次select( “由函数的实现select”,如Norman所指出的 )

因此,为什么存在data定义允许任何 a是因为数据构造函数是一个多态函数

 MkT :: forall a. a -> T 

一种MkT :: a -> *

这意味着任何a可能被应用于该function。 与之相对,比如说,一个多态

 valueT :: forall a. [a] 

一种值T :: a

这意味着valueT的定义必须是多态的。 在这种情况下, valueT可以被定义为所有types的空list []

 [] :: [t] 

差异

即使ExistentialQuantification的含义在ExistentialQuantification RankNTypeRankNType是一致的,存在也是有区别的,因为data构造函数可以用在模式匹配中。 正如ghc用户指南中所述 :

当模式匹配时,每个模式匹配为每个存在typesvariables引入一个新的,不同的types。 这些types不能与其他types统一,也不能脱离模式匹配的范围。

任何人都可以用清晰,简单的英语(或者,如果存在的话,指出我错过的一个明确的解释)完全解释forall关键字,并不假定我是一个沉浸在行话中的math家?

我将尝试在Haskell及其types系统的背景下解释所有的含义和可能的应用。

但在你明白之前,我想引导你一个由Runar Bjarnason发表的题为“ 限制解放,自由约束 ”的非常好的谈话。 这个演讲充满了来自真实世界用例的例子,以及斯卡拉的例子来支持这个声明,尽pipe它没有提到所有的例子。 我将尝试解释下面的全部观点。

  CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN 

消化和相信这个声明是非常重要的,继续下面的解释,所以我敦促你看这个讲话(至less是部分内容)。

现在,一个非常常见的例子,显示了Haskelltypes系统的performance力是这种types的签名:

foo :: a -> a

据说给定这种types的签名,只有一个函数可以满足这个types,那就是identity函数或者是更普遍已知的id

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

 foo 5 = 6 foo True = False 

他们都满足上面的types签名,那么为什么Haskell人声称它是唯一的id满足types签名?

这是因为在types签名中隐藏了一个隐含的方法。 实际的types是:

 id :: forall a. a -> a 

那么,现在让我们回到金句: 限制解放,自由约束

将其转换为types系统,该语句变为:

types层面的约束成为术语层面的自由

types层面上的自由,成为学期层面的约束


让我们试图certificate第一个陈述:

types级别的约束

所以对我们的types签名加以限制

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

在术语层面上成为一种自由让我们自由或灵活地写出所有这些

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

同样可以通过限制与任何其他types的Bool[Char]等等来观察

那么现在这个types签名是什么: foo :: (Num a) => a -> a转换为:

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

这被称为存在性量化,这意味着存在一些函数,当某个函数被馈入某种types的a返回types相同的实例时,这些实例都属于这个数字集合。

因此,我们可以看到增加一个约束( a应该属于数字集合),释放术语级别以具有多个可能的实现。


现在来看第二个陈述,实际上是对forall的解释:

types层面上的自由,成为学期层面的约束

所以,现在让我们解放types级别的function:

 foo :: forall a. a -> a 

现在这转换为:

 ∀a , a -> a 

这意味着这种types签名的实施应该是对所有情况都是一样的。

所以现在这开始限制我们在任期水平。 我们不能再写了

 foo 5 = 7 

因为这个实现不能满足,如果我们把a作为Boola可以是Char[Char]或自定义数据types。 在任何情况下,它都应该返回类似的东西。 这种types层面的自由是所谓的普遍量化,唯一可以满足这个要求的function是

 foo a = a 

这通常被称为identityfunction


因此,全部是types层面的liberty ,其实际目的是将术语层次constrain在特定的实现。