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 ?
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