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

On Wed, Sep 16, 2009 at 11:58 AM, Cristiano Paris 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

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