On 27/10/06, Greg Buchholz
I thought "exists" was spelled "forall" in Haskell?
There is some confusion here, I know it had me for a long time. forall really does mean 'for all'. I think of types as sets of values with that type, and forall as an intersection of those sets. For example, forall a. a is the intersection over all types, {_|_}, that is, the type whose only value is bottom (as this is the only value common to all types). So, for example: [forall a. a] -- the list whose elements all have the type forall a. a, i.e. a list of bottom. [forall a. Show a => a] -- the list whose elements all have the type forall a. Show a => a. The Show class constraint limits the sets you intersect over (here we're only intersection over instances of Show), but _|_ is still the only value common to all these types, so this too is a list of bottom. [forall a. Num a => a] -- again, the list where each element is a member of all types that instantiate Num. This could involve numeric literals, which have the type forall a. Num a => a, as well as bottom. forall a. [a] -- all elements have some (the same) type a, which can be assumed to be any type at all by a callee. We might want to ask 'how can we get a heterogeneous list?' Well, the type of a heterogeneous list is [exists a. a], i.e. the list where all elements have type exists a. a. exists is, as you may guess, a union of types, so this is the list where all elements could take any type at all (and the types of different elements needn't be the same). This isn't equivalent to any specific forall-involving type, unless we involve datatypes. data T = forall a. MkT a This means that: MkT :: forall a. a -> T So we can pass any type we want to MkT and it'll convert it into a T. So what happens when we deconstruct a MkT value? foo (MkT x) = ... -- what is the type of x? As we've just stated, x could be of any type. That means it's a member of some arbitrary type, so has the type x :: exists a. a. In other words, our declaration for T is isomorphic to the following one: data T = MkT (exists a. a) And suddenly we have existential types. Now we can make a heterogeneous list: heteroList = [MkT 5, MkT (), MkT True] Of course, when we pattern match on heteroList we can't do anything [1] with its elements, as all we know is that they have some arbitrary type. However, if we are to introduce class constraints: data T' = forall a. Show a => MkT' a Which is isomorphic to: data T' = MkT' (exists a. Show a => a) Again the class constraint serves to limit the types we're unioning over, so that now we know the values inside a MkT' are elements of some arbitrary type _which instantiates Show_, so we can apply show to them. heteroList' = [MkT' 5, MkT' (), MkT' True] main = mapM_ print heteroList' {- prints: 5 () True -} Hope that helps. [1]: Actually, we can apply them to functions whose type is forall a. a -> R, for some arbitrary R, as these accept values of any type as a parameter. Examples of such functions: id, const k for any k. So technically, we can't do anything _useful_ with its elements. -- -David House, dmhouse@gmail.com