Haskell / GHC中的`forall`关键字是做什么的？ [英] What does the `forall` keyword in Haskell/GHC do?

问题描述

我开始了解 forall 关键字在所谓的存在类型中是如何使用的：

 数据ShowBox = forall s。 Show s => SB s 
  

然而，这只是 forall 被使用了，我简直不能把它用在这样的事情上：



  runST :: forall一个。 （全部ST ST） - > a 
  

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



  foo ::（forall a。a  - > a） - > （Char，Bool）
 bar :: forall a。 （（a  - > a） - >（char，bool））
  

code> RankNTypes 东西...

我倾向于使用清晰，无行话的英语，而不是那种语言在学术环境中正常。我试图阅读的大部分解释（我可以通过搜索引擎找到的）有这些问题：

1. 它们不完整。他们解释了使用这个关键字的一部分（比如存在类型），这让我感觉很开心，直到我阅读以完全不同的方式使用它的代码（比如 runST ， foo 和 bar 以上）。


2. 假设我已阅读离散数学，类别理论或抽象代数的任何分支的最新内容，本周很受欢迎。 （如果我再也没有阅读过查阅论文什么的实施细节这个词，那就太快了）。


3. 它们是用各种方式写成的经常会把简单的概念变成扭曲和破碎的语法和语义。
   

在实际问题上。任何人都可以用清晰，简单的英语完全解释 forall 关键字（或者，如果它存在某处，指向我错过的一个明确解释）我是一个沉浸在行话中的数学家？

---

编辑添加：

下面有两个更高质量的答案，但不幸的是我只能选择一个最好的答案。 诺曼的答案是详细而有用的以一种展现 forall 的一些理论基础的方式解释事物，同时向我展示了它的一些实际意义。 yairchu的回答覆盖区域无人其他人提到（范围型变量），并用代码和GHCi会话说明了所有的概念。我可以选择两者都是最好的。不幸的是，我不能，并且仔细查看两个答案后，我已经决定，由于说明性代码和附加说明，yairchu略微偏离了诺曼的范围。然而，这有点不公平，因为我真的需要两个答案来理解这一点，即当我看到它时， forall 不会让我产生一丝恐惧。

解决方案

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

  foob :: forall a b。 （b→b）→> b  - > （a  - > b） - >也许是 - > b 
 foob postProcess onNothin onMust mval = 
 postProcess val 
其中
 val :: b 
 val =也许onNothin onjust mval 
  

这段代码不会在纯粹的Haskell 98中编译（语法错误）。它需要一个扩展来支持 forall 关键字。

基本上， forall 不同的 $ c>关键字（或者至少如此似乎），并且每个都有自己的Haskell扩展： ScopedTypeVariables ， RankNTypes / Rank2Types ， ExistentialQuantification 。

上面的代码没有得到任何启用的语法错误，但只有 ScopedTypeVariables 启用了类型检查。

作用域类型变量：

作用域类型变量有助于指定 / code>子句。它使得 val :: b 中的 b 与 b 在 foob :: forall a b。 （b→b）→> b - > （a - > b） - >也许是 - > b 。

令人困惑的一点：您可能会听到当您省略 它实际上仍然隐含在那里。 （来自Norman的回答：通常这些语言省略来自多态类型）。此声明是正确的，但指的是 forall 的其他用途，而不是指向 ScopedTypeVariables


Rank-N-Types：

与 mayb :: b - > （a - > b） - >也许是 - > b 相当于 mayb :: forall a b。 b - > （a - > b） - >也许是 - > b ，除< ScopedTypeVariables 以外。

这意味着它适用于每个 a 和 b 。

  ghci>让putInList x = [x] 
 ghci> liftTup putInList（5，Blah）
（[5]，[Blah]）
  

这个 liftTup 的类型必须是什么？它是 liftTup ::（forall x。x - > f x） - > （a，b）→> （f a，f b）。为了明白为什么，我们试着对它进行编码：

  ghci>让liftTup liftFunc（a，b）=（liftFunc a，liftFunc b）
 ghci> liftTup（\ x  - > [x]）（5，Hello）
没有用于（Num [Char]）的实例
 ... 
 ghci> - 嗯？ 
 ghci> ：t liftTup 
 liftTup ::（t  - > t1） - > （t，t） - > （t1，t1）
  

嗯，为什么GHC推断元组必须包含两个同样的类型？让我们告诉它它们不一定是

   -  test.hs 
 liftTup :: （x  - > fx） - > （a，b）→> （f a，f b）
 liftTup liftFunc（t，v）=（liftFunc t，liftFunc v）
 
 ghci> ：l test.hs 
对于推断类型'b'，b不能匹配预期类型'x'
 ... 
  

嗯。所以这里ghc不让我们在 v 上应用 liftFunc ，因为 v :: b 和 liftFunc 需要 x 。我们真的希望我们的函数得到一个接受任何可能的函数 x ！

  { - ＃LANGUAGE RankNTypes＃ - } 
 liftTup ::（forall x。x  - > fx） - > （a，b）→> （fa，fb）
 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）=长度x 
 
 ghci> ：l test.hs 
 ghci> eqListLen $ EQList [Hello，World] 
 2 
  

from Rank-N-Types？

  ghci> ：set -XRankNTypes 
 ghci>长度（[Hello，World] :: forall a。[a]）
难以匹配预期的类型'a'['Char]'
 ... 
  

在Rank-N-Types中，所有a 表示您的表达式必须适合所有可能的 a s。例如：



  ghci> length（[] :: forall a。[a]）
 0 
  

一个空列表确实可以作为任何类型的列表。

因此，通过存在量化， forall s在 data 定义表示，所包含的值可以是任何适合的类型，而不是必须是所有适合的类型。

I'm beginning to understand how the forall keyword is used in so-called "existential types" like this:

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

This is only a subset, however, of how forall is used and I simply cannot wrap my mind around its use in things like this:

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

Or explaining why these are different:

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

Or the whole RankNTypes stuff...

I tend to prefer clear, jargon-free English rather than the kinds of language which are normal in academic environments. Most of the explanations I attempt to read on this (the ones I can find through search engines) have these problems:

1. They're incomplete. They explain one part of the use of this keyword (like "existential types") which makes me feel happy until I read code that uses it in a completely different way (like runST, foo and bar above).
2. They're densely packed with assumptions that I've read the latest in whatever branch of discrete math, category theory or abstract algebra is popular this week. (If I never read the words "consult the paper whatever for details of implementation" again, it will be too soon.)
3. They're written in ways that frequently turn even simple concepts into tortuously twisted and fractured grammar and semantics.

So...

On to the actual question. Can anybody completely explain the forall keyword in clear, plain English (or, if it exists somewhere, point to such a clear explanation which I've missed) that doesn't assume I'm a mathematician steeped in the jargon?

---

Edited to add:

There were two stand-out answers from the higher-quality ones below, but unfortunately I can only choose one as best. Norman's answer was detailed and useful, explaining things in a way that showed some of the theoretical underpinnings of forall and at the same time showing me some of the practical implications of it. yairchu's answer covered an area nobody else mentioned (scoped type variables) and illustrated all of the concepts with code and a GHCi session. Were it possible to select both as best, I would. Unfortunately I can't and, after looking over both answers closely, I've decided that yairchu's slightly edges out Norman's because of the illustrative code and attached explanation. This is a bit unfair, however, because really I needed both answers to understand this to the point that forall doesn't leave me with a faint sense of dread when I see it in a type signature.

解决方案

Let's start with a code example:

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

This code doesn't compile (syntax error) in plain Haskell 98. It requires an extension to support the forall keyword.

Basically, there are 3 different common uses for the forall keyword (or at least so it seems), and each has its own Haskell extension: ScopedTypeVariables, RankNTypes/Rank2Types, ExistentialQuantification.

The code above doesn't get a syntax error with either of those enabled, but only type-checks with ScopedTypeVariables enabled.

Scoped Type Variables:

Scoped type variables helps one specify types for code inside where clauses. It makes the b in val :: b the same one as the b in foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

A confusing point: you may hear that when you omit the forall from a type it is actually still implicitly there. (from Norman's answer: "normally these languages omit the forall from polymorphic types"). This claim is correct, but it refers to the other uses of forall, and not to the ScopedTypeVariables use.

Rank-N-Types:

Let's start with that mayb :: b -> (a -> b) -> Maybe a -> b is equivalent to mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, except for when ScopedTypeVariables is enabled.

This means that it works for every a and b.

Let's say you want to do something like this.

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

What's must be the type of this liftTup? It's liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). To see why, let's try to code it:

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)

"Hmm.. why does GHC infer that the tuple must contain two of the same type? Let's tell it they don't have to be"

-- 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'
    ...

Hmm. so here ghc doesn't let us apply liftFunc on v because v :: b and liftFunc wants an x. We really want our function to get a function that accepts any possible x!

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

So it's not liftTup that works for all x, it's the function that it gets that does.

Existential Quantification:

Let's use an example:

-- 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

How is that different from Rank-N-Types?

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

With Rank-N-Types, forall a meant that your expression must fit all possible as. For example:

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

An empty list does work as a list of any type.

So with Existential-Quantification, foralls in data definitions mean that, the value contained can be of any suitable type, not that it must be of all suitable types.

这篇关于Haskell / GHC中的`forall`关键字是做什么的？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！