On 27/10/06, Greg Buchholz wrote:

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

On 10/27/06, David House wrote:

On 27/10/06, David House wrote:

...

heteroList' = [MkT' 5, MkT' (), MkT' True] main = mapM_ print heteroList'

{- prints: 5 () True -}

Sorry, the definition of main is a bit off. It should read:

main = mapM_ (\(MkT' x) -> print x) heteroList'

Of course you have to unpack the MkT' first (or define a Show instance for T', noting that you can't derive anything on existentials).

So you specified that the types which T' wraps up should be instances of Show, so to me it makes sense that you should be able to derive Show in a way similar to how newtype deriving works. But perhaps there is a subtlety that I'm missing? I mean, to make an instance of Show I'm just going to type something trivial like this: instance Show T' where show (MkT' a) = "MkT' " ++ show a Or perhaps, since I'm writing it by hand I'd omit the "MkT' " and just show the a. thanks, Jason

"David House" writes:

On 27/10/06, Greg Buchholz wrote:

...

I thought "exists" was spelled "forall" in Haskell?

There is some confusion here,

It's the notation for data declarations that causes the confusion. To rearrange your text a bit:

So, for example:

[forall a. a] -- the list whose elements all have the type forall a. a, i.e. a list of bottom.

list of bottoms.

forall a. [a] -- all elements have some (the same) type a, which can be assumed to be any type at all by a callee.

and consequently also must be a list of bottoms. This:

data T = forall a. MkT a

is where the confusion comes in.

This means that:

MkT :: forall a. a -> T

If the standard syntax were

data T where MkT :: forall a. a -> T

(as for GADTs), there's be less of a problem. (it's still misleading, because T looks like it has no variables in it, which might lead one to conclude that MkT throws away its argument) Equally, the natural way of writing it with the old syntax would be:

data T = MkT (exists a. a)

ie a T is the constructor MkT applied to some unknown type. So people seeing the first form tend to think it means this last. -- which is what you said, but I think this highlights the source of confusion better. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk