Cristiano Paris wrote:
On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <ryani.s...@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.
It's not existential, it's rank-2 universal. The first function is
saying that "for every type, a, there is a function, te...@a, taking a
into Int". This is very different than the second function which says
"there is a function, test2, taking values which belong to all types
into Int". The test2 function is not polymorphic, instead it takes
arguments which are polymorphic.
Since _|_ is the only inhabitant of all types, it may be helpful to
consider these functions instead:
f :: forall a. (a -> a) -> Int
g :: (forall a. a -> a) -> Int
The function f takes a monomorphic function of type (a->a) for some
predefined a. Which a? Well it can be any of them, but it can only be
one of them at a time. That is, the invocation of f will make the a
concrete.
The function g takes a polymorphic function which, being polymorphic,
will work for every a. That is, the invocation of g does not make the
type concrete; only the invocation of the argument within the body of g
will make the type concrete. Moreover, the argument must be able to be
made concrete for every a, it can't pick and choose. This is different
from existential quantification which means the argument works for some
a, but it won't tell us which one.
To put it another way, this is a valid definition of g:
(\ r -> let _ = r Nothing ; _ r "hello" in 42)
Since r is polymorphic, we can use it at two different types. Whereas if
we gave this definition for f it wouldn't type check since we can't
unify (Maybe a) and String.
Or, to put it another way, since there are no non-bottom objects of type
(forall a. a):
Why?
By definition of Haskell semantics. The only value belonging to all
types is _|_ (whether undefined or various exception bottoms).
Perhaps it'd make more sense to look at another type. What values
inhabit (forall a. Maybe a)? Well _|_ inhabits all types, so it's there.
And Nothing doesn't say anything about a, so it's there too since it
works for all a. And (Just _|_) is there since Just doesn't say anything
about the type a and _|_ belongs to all types so it doesn't say anything
about a either. And that's it. Any other value must say something about
the type a, thus restricting it, and then it would no longer be
universally quantified.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
