What does the `forall` keyword in Haskell/GHC do?

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:

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 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 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 -> fx) -> (a, b) -> (fa, fb) . 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 a s. For example:

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

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

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

Can anybody completely explain the forall keyword in clear, plain English?

No. (Well, maybe Don Stewart can.)

Here are the barriers to a simple, clear explanation or forall :

As for your particular examples,

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

Summary: A complete explanation of the forall keyword requires math and can be understood only by someone who has studied the math. Even partial explanations are hard to understand without math. But maybe my partial, non-math explanations help a little. Go read Launchbury and Peyton Jones on runST !

Addendum: Jargon "above", "below", "to the left of". These have nothing to do with the textual ways types are written and everything to do with abstract-syntax trees. In the abstract syntax, a forall takes the name of a type variable, and then there is a full type "below" the forall. An arrow takes two types (argument and result type) and forms a new type (the function type). The argument type is "to the left of" the arrow; it is the arrow's left child in the abstract-syntax tree.

Examples:

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

My original answer:

Can anybody completely explain the forall keyword in clear, plain English

As Norman indicates, it is very hard to give a clear, plain English explanation of a technical term from type theory. We're all trying though.

There is only really one thing to remember about 'forall': it binds types to some scope . Once you understand that, everything is fairly easy. It is the equivalent of 'lambda' (or a form of 'let') on the type level -- Norman Ramsey uses the notion of "left"/"above" to convey this same concept of scope in his excellent answer.

Most uses of 'forall' are very simple, and you can find them introduced in the GHC Users Manual, S7.8., particularly the excellent S7.8.5 on nested forms of 'forall'.

In Haskell, we usually leave off the binder for types, when the type is universally quanitified, like so:

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

is equivalent to:

length :: [a] -> Int

That's it.

Since you can bind type variables now to some scope, you can have scopes other than the top level ("universally quantified"), like your first example, where the type variable is only visible within the data structure. This allows for hidden types ("existential types"). Or we can have arbitrary nesting of bindings ("rank N types").

To deeply understand type systems, you will need to learn some jargon. That's the nature of computer science. However, simple uses, like above, should be able to be grasped intuitively, via analogy with 'let' on the value level. A great introduction is Launchbury and Peyton Jones.

上一篇: Haskell中的孤立实例

下一篇: Haskell / GHC中的`forall`关键字是做什么的？