quantified types (forall/exist):
an easy way to memorize this is to think of 'forall' as a big 'and'
and of 'exists' as a big 'or'.
e :: forall a. a -- e has type 'Int' and type 'Bool' and type ..
e :: exists a. a -- e has type 'Int' or type 'Bool' or type ..
That doesn't entirely make sense. (What am I on about? That doesn't
make *any* sense...)
indeed?-) then you've probably already figured out what those types
mean! there aren't many variations of an expression that has *all* types
("you can't please everyone"), and if an expression has a type but we
have no way of knowing what that type is, there isn't much we can do
with it (like advice from the Oracle of Delphi). but both of these
kinds of quantified types make a lot more sense in larger contexts.
lets take 'forall'/'big and' first: the problem with 'forall a. a' is to
produce something that is everything to everyone, which is rather hard;
but what about 'forall a. a -> a'? that is like a general shipping
agency - they don't care what you give them, they just put it in a box
and move it from one place to another (if it doesn't like to be shipped
in such an indifferent way, it'll break, but that's not their problem);
such general shipping is both 'Integer' shipping *and* 'String' shipping
*and* ..; other examples are 'forall a. a -> a -> a', which is a general
selector (given two 'a's, it returns one of them), or
'forall a,b. a -> b -> a' (given an 'a' and a 'b', it returns the 'a').
'id :: forall a. a -> a' can be instantiated to 'id :: Bool -> Bool'
*and* to 'id :: Char -> Char' *and* to all other identities on rank-1
types besides, so one could say that it really has *all* of those types.
what about 'exists'/'big or' then? the problem with 'exists a. a' is
that while we know there exists a type, we have no way of knowing
what that type is, so we can't really do anything with an expression
of such a type.
that is very much like an abstract data type, implemented on top
of a hidden representation type. what we need are some operations
on that abstract type, so how about
'exists r.(r a, r a -> a -> r a, r a -> a)'
we still don't know what 'r' is, but we have some 'r a', we have a way
to combine 'r a' and 'a' into a new 'r a', and a way to extract an 'a'
from an 'r a', so we're no longer entirely helpless. in fact, that looks
a lot like an abstract container type, perhaps a stack with push and
top, or a queue with add and front, or a cell with put and get.
whatever it may be, the 'r' is hidden, so it could be
'([a], [a]->a->[a], [a]->a)'
*or* it could be
'(Set a, Set a -> a -> Set a, Set a -> a)'
*or* it could be based on *any* other rank-1 type constructor.
oracle advice: 'invade :: exists great_empire. great_empire -> ()'
Haskell-Cafe mailing list