On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram <ryani.s...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe