[Haskell-cafe] Re: Rank N type tutorial?

"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