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

Question

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.

Answer 1

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

Er, and what about simple first-order logic? forall is pretty clearly in reference to universal quantification, and in that context the term existential makes more sense as well, though it would be less awkward if there were an exists keyword. Whether quantification is effectively universal or existential depends on the placement of the quantifier relative to where the variables are used on which side of a function arrow and it's all a bit confusing.

So, if that doesn't help, or if you just don't like symbolic logic, from a more functional programming-ish perspective you can think of type variables as just being (implicit) type parameters to the function. Functions taking type parameters in this sense are traditionally written using a capital lambda for whatever reason, which I'll write here as /\.

So, consider the id function:

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

We can rewrite it as lambdas, moving the "type parameter" out of the type signature and adding inline type annotations:

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

Here's the same thing done to const:

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

So your bar function might be something like this:

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

Note that the type of the function given to bar as an argument depends on bar's type parameter. Consider if you had something like this instead:

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

Here bar2 is applying the function to something of type Char, so giving bar2 any type parameter other than Char will cause a type error.

On the other hand, here's what foo might look like:

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

Unlike bar, foo doesn't actually take any type parameters at all! It takes a function that itself takes a type parameter, then applies that function to two different types.

So when you see a forall in a type signature, just think of it as a lambda expression for type signatures. Just like regular lambdas, the scope of forall extends as far to the right as possible, up to enclosing parenthesis, and just like variables bound in a regular lambda, the type variables bound by a forall are only in scope within the quantified expression.

---

Post scriptum: Perhaps you might wonder--now that we're thinking about functions taking type parameters, why can't we do something more interesting with those parameters than put them into a type signature? The answer is that we can!

A function that puts type variables together with a label and returns a new type is a type constructor, which you could write something like this:

Either = /\a b -> ...

But we'd need completely new notation, because the way such a type is written, like Either a b, is already suggestive of "apply the function Either to these parameters".

On the other hand, a function that sort of "pattern matches" on its type parameters, returning different values for different types, is a method of a type class. A slight expansion to my /\ syntax above suggests something like this:

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]

Personally, I think I prefer Haskell's actual syntax...

A function that "pattern matches" its type parameters and returns an arbitrary, existing type is a type family or functional dependency--in the former case, it even already looks a great deal like a function definition.

Answer 2

The reason why there are different uses of this keyword is that it's actually used in at least two different type system extensions: higher-rank types, and existentials.

It's probably best just to read about and understand those two things separately, rather than trying to get an explanation of why 'forall' is an appropriate bit of syntax in both at the same time.

Answer 3

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.

Answer 4

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.