[Haskell-cafe] How to understand the 'forall' ?
ryani.spam at gmail.com
Thu Sep 17 02:36:55 EDT 2009
On Wed, Sep 16, 2009 at 11:58 AM, Cristiano Paris <frodo at theshire.org>wrote:
> On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <ryani.spam at 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
> > 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.
> 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
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):
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 :)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe