What is the difference between forall a. [a] and [forall a. a]?

Question

Title and tags should explain the question adequately.

Answer 1

The type forall a. [a] means that for any single type, it's a list containing that type. This is also what just plain [a] means and is the type of [], the empty list data constructor.

The type [forall a. a] would mean that you have a list of values with polymorphic type, that is, each one is a value of any possible type, not necessarily the same as other elements of the list. No possible value can have the type forall a. a, so this must also be an empty list.

The difference, then, is that while the first can be used as a list of any type (by definition, basically), the latter can't be used as a list of any concrete type at all, since there's no way to pin it down to any single type.

To address the tag--an existential type is one that, within some scope, will be instantiated to some unknown concrete type. It could be anything, so is represented by something like the forall a. a above. To make sure that anything with an existential type is only used within the scope where the actual type will be available, the compiler prevents existential types from "escaping".

It may help to think of the forall quantifier as being like a lambda expression--it introduces a new type variable and binds that identifier within some scope. Outside that scope, the identifier has no meaning, which is why forall a. a is pretty useless.

Answer 2

When used for types forall means intersection. So forall a. a is the intersection of all types or something like Int ∩ String ∩ ... which seems to give the empty set but each type has an extra element called bottom or ⊥ or undefined in Haskell. From this we get that forall a. a = {⊥}. Actually we can define a type which contains only bottom:

data Zero

After this setup lets look at our types starting with [forall a. a]. What it defines is a list of bottoms or [Zero] which has elements [], [undefined], [undefined, undefined], .... Lets check it in ghci:

> let l = [undefined, undefined]::[Zero]
> :t l
l :: [Zero]

In a similar way forall a. [a] is the intersection of all list types and since ∩[a] = [∩a] this is again [Zero].

To do a final check lets define:

type L = forall a. [a]
type U = [forall a. a]

and in ghci:

> let l2 = [undefined, undefined]::L
> let l3 = [undefined, undefined]::U
> :t l2
l2 :: [a]
> :t l3
l3 :: U

Notice that l2::[a], the explanation is that Haskell puts an implicit forall in front of all polymorphic types.

Answer 3

Title and tags should explain the question adequately.

Err, not really. You used the tag existential-type, but neither of the types you gave is existential.

System F

There's already some good answers here, so I'll take a different approach and be a bit more formal. Polymorphic values are essentially functions on types, but Haskell's syntax leaves both type abstraction and type application implicit, which obscures the issue. We'll use the notation of System F, which has explicit type abstraction and type application.

For example, the familiar map function would be written

map :: ∀a. ∀b. (a → b) → [a] → [b]
map = Λa. Λb. λ(f :: a → b). λ(xs :: [a]). case xs of
  [] → []
  (y:ys) → f y : map @a @b f ys

map is now a function of four arguments: two types (a and b), a function, and a list. We write a function over types using Λ (upper-case lambda), and a function over values using λ as usual. A term containing Λ gives rise to a type containing ∀, just as a term containing λ gives rise to a type containing →. I use the notation @a (as in GHC Core) to denote application of a type argument.

So a value of polymorphic type is like a function from types to values. The caller of a polymorphic function gets to choose a type argument, and the function must comply.

∀a. [a]

How, then, would we write a term of type ∀a. [a]? We know that types containing ∀ come from terms containing Λ:

term1 :: ∀a. [a]
term1 = Λa. ?

Within the body marked ? we must provide a term of type [a]. That is, a term of type ∀a. [a] means "given any type a, I will give you a list of type [a]".

However, we know nothing concrete about a, since it's an argument passed in from the outside. So we can return an empty list

term1 = Λa. []

or an undefined value

term1 = Λa. undefined

or a list containing undefined values only

term1 = Λa. [undefined, undefined]

but not much else.

[∀a. a]

What about [∀a. a], then? If ∀ signifies a function on types, then [∀a. a] is a list of functions. We can provide as few as we like:

term2 :: [∀a. a]
term2 = []

or as many:

term2 = [f, g, h]

But what are our choices for f, g, and h?

f :: ∀a. a
f = Λa. ?

Now we're well and truly stuck. We have to provide a value of type a, but we know nothing whatsoever about the type a. So our only choice is

f = Λa. undefined

So our options for term2 look like

term2 :: [∀a. a]
term2 = []
term2 = [Λa. undefined]
term2 = [Λa. undefined, Λa. undefined]

etc. And let's not forget

term2 = undefined

Existential types

A value of universal (∀) type is a function from types to values. A value of existential (∃) type is a pair of a type and a value.

More specifically: A value of type

∃x. T

is a pair

(S, v)

where S is a type, and where v :: T, assuming you bind the type variable x to S within T.

Here's an existential type signature and a few terms with that type:

term3 :: ∃a. a
term3 = (Int,         3)
term3 = (Char,        'x')
term3 = (∀a. a → Int, Λa. λ(x::a). 4)

In other words, we can put any value we like into ∃a. a, as long as we pair that value with its type.

The user of a value of type ∀a. a is in a great position; they can choose any specific type they like, using the type application @T, to obtain a term of type T. The producer of a value of type ∀a. a is in a terrible position: they must be prepared to produce any type asked for, so (as in the previous section) the only choice is Λa. undefined.

The user of a value of type ∃a. a is in a terrible position; the value inside is of some unknown specific type, not a flexible polymorphic value. The producer of a value of type ∃a. a is in a great position; they can stick any value they like into the pair, as we saw above.

So what's a less useless existential? How about values paired with a binary operation:

type Something = ∃a. (a, a → a → a, a → String)

term4_a, term4_b :: Something
term4_a = (Int,    (1,     (+)  @Int , show @Int))
term4_b = (String, ("foo", (++) @Char, λ(x::String). x))

Using it:

triple :: Something → String
triple = λ(a, (x :: a, f :: a→a→a, out :: a→String)).
  out (f (f x x) x)

The result:

triple term4_a  ⇒  "3"
triple term4_b  ⇒  "foofoofoo"

We've packaged up a type and some operations on that type. The user can apply our operations but cannot inspect the concrete value — we can't pattern-match on x within triple, since its type (hence set of constructors) is unknown. This is more than a bit like object-oriented programming.

Using existentials for real

The direct syntax for existentials using ∃ and type-value pairs would be quite convenient. UHC partially supports this direct syntax. But GHC does not. To introduce existentials in GHC we need to define new "wrapper" types.

Translating the above example:

{-# LANGUAGE ExistentialQuantification #-}

data Something = forall a. MkThing a (a -> a -> a) (a -> String)

term_a, term_b :: Something
term_a = MkThing 1 (+) show
term_b = MkThing "foo" (++) id

triple :: Something -> String
triple (MkThing x f out) =
  out (f (f x x) x)

There's a couple differences from our theoretical treatment. Type application, type abstraction, and type pairs are again implicit. Also, the wrapper is confusingly written with forall rather than exists. This references the fact that we're declaring an existential type, but the data constructor has universal type:

MkThing :: forall a. a -> (a -> a -> a) -> (a -> String) -> Something

Often, we use existential quantification to "capture" a typeclass constraint. We could do something similar here:

data SomeMonoid = forall a. (Monoid a, Show a) => MkMonoid a

Further reading

For an introduction to the theory, I highly recommend Types and Programming Languages by Pierce. For a discussion of existential types in GHC, see the GHC manual and the Haskell wiki.