Quantification in Haskell

I wrote an answer over at Stack Overflow that somehow grew to article length. Here it is, recorded for posterity.

I'll paraphrase the original question as:

• What's the difference between the types forall a. [a] and [forall a. a], and

• How does this relate to existential types?

Well, the short answer to the second question is "It doesn't relate". But there's still a natural flow in discussing both topics.

Notation

Polymorphic values are essentially functions on types, but Haskell's syntax leaves both type abstraction and type application implicit. To better understand what's going on, we'll use a pidgin syntax of Haskell combined with a typed lambda calculus like System F.

In System F, polymorphism involves explicit type abstractions and type application. For example, the familiar map function would be written as:

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: types a and b, a function, and a list.

At the term level, we have one new syntactic form: Λ (upper-case lambda). A polymorphic value is a function from types to values, written Λx. e, much as a function from values to values is written λx. e.

At the type level, we have the symbol ∀ ("for all"), corresponding to GHC's forall keyword. A term containing Λ gives rise to a type containing ∀, just as a term containing λ gives rise to a type containing →.

Since we have functions of types, we also need application of types. I use the notation @a (as in GHC Core) to denote application of a type argument. So we might use map like so:

map @Char @Int ord "xzy"

Note also that I've provided an explicit type on each λ abstraction. Type inference for System F is, in general, undecidable (Wells, 1999). The restricted form of polymorphism available in vanilla Haskell 98 has decidable inference, but you lose this if you enable certain GHC extensions like RankNTypes.

We don't need annotations on Λ abstractions, because we have only one "kind" of type. In actual Haskell, or a calculus like System Fω, we also have type constructors, and we need a system of kinds to describe how they combine. We'll ignore this issue here.

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.

One last bit of notation: I'll use the syntax

⊥@t

to mean an undefined value of type t, similar to Haskell's undefined.

∀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]. 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. ⊥@[a]

or a list containing undefined values only

term1 = Λa. [⊥@a, ⊥@a]

but not much else.

To use this value, we apply a type, removing the outer ∀. Let's arbitrarily instantiate ∀a. [a] to [Bool]:

main = print @Int (length @Bool (term1 @Bool))

[∀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. ⊥@a

So our options for term2 look like

term2 :: [∀a. a]
term2 = []
term2 = [Λa. ⊥@a]
term2 = [Λa. ⊥@a, Λa. ⊥@a]

etc. And let's not forget

term2 = ⊥@(∀a. [a])

Unlike the previous example, our choices for term2 are already lists, and we can pass them to length directly. As before, we have to pass the element type to length:

main = print @Int (length @(∀a. a) term2)

Existential types

So 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. ⊥@a.

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 type class 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.