[Haskell-cafe] How to understand the 'forall' ?

[wren ng thornton]

Cristiano Paris wrote:
> On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:
>> Here's the difference between these two types:
>>
>> test1 :: forall a. a -> Int
>> -- The caller of test1 determines the type for test1
>> test2 :: (forall a. a) -> Int
>> -- The internals of test2 determines what type, or types, to instantiate the
>> argument at
> 
> I can easily understand your explanation for test2: the type var a is
> closed under existential (?) quantification. I can't do the same for
> test1, even if it seems that a is closed under universal (?)
> quantification as well.

It's not existential, it's rank-2 universal. The first function is 
saying that "for every type, a, there is a function, test1 at a, taking a 
into Int". This is very different than the second function which says 
"there is a function, test2, taking values which belong to all types 
into Int". The test2 function is not polymorphic, instead it takes 
arguments which are polymorphic.

Since _|_ is the only inhabitant of all types, it may be helpful to 
consider these functions instead:

     f :: forall a. (a -> a) -> Int
     g :: (forall a. a -> a) -> Int

The function f takes a monomorphic function of type (a->a) for some 
predefined a. Which a? Well it can be any of them, but it can only be 
one of them at a time. That is, the invocation of f will make the a 
concrete.

The function g takes a polymorphic function which, being polymorphic, 
will work for every a. That is, the invocation of g does not make the 
type concrete; only the invocation of the argument within the body of g 
will make the type concrete. Moreover, the argument must be able to be 
made concrete for every a, it can't pick and choose. This is different 
from existential quantification which means the argument works for some 
a, but it won't tell us which one.

To put it another way, this is a valid definition of g:

     (\ r -> let _ = r Nothing ; _ r "hello" in 42)

Since r is polymorphic, we can use it at two different types. Whereas if 
we gave this definition for f it wouldn't type check since we can't 
unify (Maybe a) and String.


>> Or, to put it another way, since there are no non-bottom objects of type
>> (forall a. a):
> 
> Why?

By definition of Haskell semantics. The only value belonging to all 
types is _|_ (whether undefined or various exception bottoms).

Perhaps it'd make more sense to look at another type. What values 
inhabit (forall a. Maybe a)? Well _|_ inhabits all types, so it's there. 
And Nothing doesn't say anything about a, so it's there too since it 
works for all a. And (Just _|_) is there since Just doesn't say anything 
about the type a and _|_ belongs to all types so it doesn't say anything 
about a either. And that's it. Any other value must say something about 
the type a, thus restricting it, and then it would no longer be 
universally quantified.

-- 
Live well,
~wren