On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram
... 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