[Haskell-cafe] Rank N type tutorial?

[David House]

On 27/10/06, Greg Buchholz <haskell at sleepingsquirrel.org> 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 at gmail.com