forall is often referred to existential types in Haskell, but why?
Let's start by motivating universal types first (TAPL, Chapter 23).
We want universal types because we want polymorphism.
Suppose we have a definition id = \x -> x, we want it to work for all types.
We are actually very comfortable with this idea in Haskell:
*Main> :t id
id :: a -> a
Now we see a free variable a in the type of id. We are told that a is a type variable. In fact, the type variable a is implicitly bound and we can make it explicit:
*Main> :set -fglasgow-exts
*Main> :t id
id :: forall a. a -> a
Now this is a paragraph only of theoretical interests. If the polymorphism supports only monomorphic types (e.g. Int, Float), it's called predicative. If it supports all types (e.g. the type of id), it's called impredicative. I can vaguely recall that ML imposes value restriction but I'm not exactly sure about the details:
Objective Caml version 3.10.0
# let id = fun x -> x;;
val id : 'a -> 'a =
# let q = id id;;
val q : '_a -> '_a =
# q 3;;
- : int = 3
# q;;
- : int -> int =
# q 3.0;;
This expression has type float but is here used with type int
OK, predicativeness is not the point of this post. We know we still get a polymorphic function by applying id to id in Haskell. Back to forall, we infer the type of a function based on its definition. Sometimes we can say something about the inhabitants of a type too. For now we ignore undefined, the bottom of any types, often written as _|_.
What can be typed forall a. a? In other words, it can be typed as anything. The answer is nothing.
What can be typed forall a. a -> a? In other words, it's a function that can be applied to any types. Without looking into its argument, all it can do is to simply return the argument. Therefore, there is only one value of this type, the id function.
Let's add constraints to the type variable. What can be typed forall a. (Num a) => a -> a? A lot. Because now you know there are functions usable for the type variable. You can make (+2), (*3), etc. out of a's interface.
Move on to existential types. Existential types are originally proposed to formalize ADTs or modules (TAPL, Chapter 24). An existential type is written as {exists X, T}. T can be thought of as a signature, and an element of such existential type is a witness of the truth of the existence, or an instance of the signature.
Existentials can be encoded with universals (TAPL, Section 24.3). But according to the EHC project, existentials in Haskell are encoded in an simplified way using forall, and so is restricted to data declarations. The conversion between exists and forall is shown here.
To understand the conversion better, let's not forget this rule in logic:
forall x. ( P ( x ) -> Q ) <==> ( exists x. P ( x ) ) -> Q
Cast it into Haskell we get:
forall a. ( Constructor a -> Datatype) <==> (exists a. Constructor a) -> Datatype
Which converts data T = forall a. MkT a into data T = MkT (exists a. a).
Why is it useful? Frankly I don't know yet. At least it's used to encode heterogenous lists in a Scheme implementation.
I know it's fun, but please don't ask about Curry-Howard isomorphism....