forall as an intersection over those sets

Question

I have been reading the existential section on Wikibooks and this is what is stated there:

Firstly, forall really does mean 'for all'. One way of thinking about types is as sets of values with that type, for example, Bool is the set {True, False, ⊥} (remember that bottom, ⊥, is a member of every type!), Integer is the set of integers (and bottom), String is the set of all possible strings (and bottom), and so on. forall serves as an intersection over those sets. For example, forall a. a is the intersection over all types, which must be {⊥}, that is, the type (i.e. set) whose only value (i.e. element) is bottom.

How does forall serve as an intersection over those sets ?

forall in formal logic means that it can be any value from the universe of discourse. How does in Haskell it gets translated to intersection ?

Answer 1

How does forall serve as an intersection over those sets ?

Here you may benefit from starting to read a bit about the Curry-Howard correspondence. To make a long story short, you can think of a type as a logical proposition, language expressions as proofs of their types, and values as normal form proofs (proofs that cannot be simplified any further). So for example, "Hello world!" :: String would be read as ""Hello world!" is a proof of the proposition String."

So now think of forall a. a as a proposition. Intuitively, think of this as a second-order quantified statement over a propositional variable: "For all statements a, a." It's basically asserting all propositions. This means that if x is a proof of forall a. a, then for any proposition P, x is also a proof of P. So, since the proofs of forall a. a are the proofs that prove any propositions, then it must follow that the proofs of forall a. a must be the same as what you'd get if you mapped each proposition to the set of its proofs and took their intersection. And the only normal-form proof (i.e. "value") that is common to all those sets is bottom.

Another informal way to look at it is that universal quantification is like an infinite conjunction (∀x.P(x) is like P(c0) ∧ P(c1) ∧ ...). Conjunction, seen from a model-theoretical view, is set intersection; the set of evaluation environments where A ∧ B is true is the intersection of the environments where A is true and the ones where B is true.

Answer 2

Haskell's forall-s can be viewed as restricted dependent function types, which I think is the conceptually most enlightening approach and also most amenable to set-theoretic or logical interpretations.

In a dependent language one can bind the values of arguments in function types, and mention those values in the return types.

-- Idris
id : (a : Type) -> (a -> a)
id _ x = x 

-- Can also leave arguments implicit (to be inferred)
id : a -> a
id x = x

-- Generally, an Idris function type has the form "(x : A) -> F x"
-- where A is a type (or kind/sort, or any level really) and F is 
-- a function of type "A -> Type" 

-- Haskell
id :: forall (a : *). (a -> a)
id x = x 

The crucial difference is that Haskell can only bind types, lifted kinds, and type constructors, using forall, while dependent languages can bind anything.

In the literature dependent functions are called dependent products. Why call them that, when they are, well, functions? It turns out that we can implement Haskell's algebraic product types using only dependent functions.

Generally, any function a -> b can be viewed as a lookup function for some product, where the keys have type a and the elements have type b. Bool -> Int can be interpreted as a pair of Int-s. This interpretation is not very interesting for non-dependent functions, since all the product fields must be of the same type. With dependent functions, our pair can be properly polymorphic:

Pair : Type -> Type -> Type 
Pair a b = (index : Bool) -> (if index then a else b) 

fst : Pair a b -> a
fst pair = pair True

snd : Pair a b -> b
snd pair = pair False

setFst : c -> Pair a b -> Pair c b
setFst c pair = \index -> if index then c else pair False

setSnd : c -> Pair a b -> Pair a c
setSnd c pair = \index -> if index then pair True else c 

We have recovered all the essential functionality of pairs here. Also, using Pair we can build up products of arbitrary arity.

So, how does is tie in to the interpretation of forall-s? Well, we can interpret ordinary products and build up some intuition for them, and then try to transfer that to forall-s.

So, let's look a bit first at the algebra of ordinary products. Algebraic types are called algebraic because we can determine the number of their values by algebra. Link to detailed explanation. If A has |A| number of values and B has |B| number of values, then Pair A B has |A| * |B| number of possible values. With sum types we sum the number of inhabitants. Since A -> B can be viewed as a product with |A| fields, all having type B, the number of the inhabitants of A -> B is |A| number of |B|-s multiplied together, which equals |B|^|A|. Hence the name "exponential type" that is sometimes used to denote functions. When the function is dependent, we fall back to the "product over some number of different types" interpretation, since the exponential formula no longer fits.

Armed with this understanding, we can interpret forall (a :: *). t as a product type with indices of type * and fields having type t, where a might be mentioned inside t, and thus the field types may vary depending on the choice of a. We can look up the fields by making Haskell infer some particular type for the forall, effectively applying the function to the type argument.

Note that this product has as many fields as many values of indices there are, which is pretty much infinite here, considering the potential number of Haskell types.

Answer 3

You have to view types in either negative or positive context—i.e. either in the process of construction or the process of use (have/receive and this is all probably best understood in Game Semantics, but I am not familiar with them).

If I "give you" a type forall a . a then you know I must have constructed it somehow. The only way for a particular constructed value to have the type forall a . a is that it could be a stand-in "for all" types in the universe of discourse—which is, of course, the intersection of their functionality. In sane languages no such value exists (Void), but in Haskell we have bottom.

bottom :: forall a . a
bottom = let a = a in a

On the other hand, if I somehow magically have a value of forall a . a and I attempt to use it then we get the opposite effect—I can treat it as anything in the union of all types in the universe of discourse (which is what you were looking for) and thus I have

absurd :: (forall a . a) -> b
absurd a = a