
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. hth, claus oracle advice: 'invade :: exists great_empire. great_empire -> ()'