On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <ryani.spam@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.

Both are universally quantified, but at a different level. To look at it in System F-land, you have two levels of types that can get passed in lambdas. 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.

In test1, the caller specifies "a" and then passes in an object of that type.
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"

> 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. For example, what could the result of

test3 :: (forall a. a) -> Int
test3 x = length (x `asTypeOf` [()])

be? How could you call it?

> test1 converts *anything* to an Int.

Is the only possible implementation of test1 the one ignoring its
argument (apart from bottom of course)?

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 :)

-- ryan