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

[Cristiano Paris]

On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram <ryani.spam at gmail.com> wrote:
> ...
> Explicitly:
>
> Haskell:
>> test1 :: forall a. a -> Int
>> test1 _ = 1
>> test2 :: (forall a. a) -> Int
>> test2 x = x
>
> explicitly in System F:
>
> test1 = /\a \(x :: a). 1
> test2 = \(x :: forall a. a). x @Int
>
> /\ is type-level lambda, and @ is type-level application.

Ok. But let me be pedantic: where is the universal quantification in
test1? It seems to me the a is a free variable in test1 while being
closed under universal quantification in test2.

> In test1, the caller specifies "a" and then passes in an object of that
> type.

The witness?

> In test2, the caller must pass in an object which is of all types, and test2
> asks for that object to be instantiated at the type "Int"

"of all types" means "a value which belongs to all the sets of all the
types", i.e. bottom?

>> > Or, to put it another way, since there are no non-bottom objects of type
>> > (forall a. a):
>>
>> Why?
>
> Informally, because you can't create something that can be any type.

Yes, I misread the initial statement. I missed the "non-bottom" part :)

> There's one way that doesn't entirely ignore its argument.
>
> test4 x = seq x 1
>
> But I don't like to talk about that one :)

:) Thank you Ryan, you were very explicative. I may say that the use
of the System-F's notation, making everything explicit, clarifies this
a bit.

Cristiano