[Haskell-cafe] Type system madness

[David Menendez]

On 7/9/07, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> OK, can somebody explain to me *really slowly* exactly what the
> difference between an existential type and a rank-N type is?

One important difference is that Hugs supports existential
quantification, but not rank-N types. (It does support rank-2 types,
which are more common.)

The ExistentialQuantification and PolymorphicComponents extensions
have to do with what's allowed when defining datatypes.

The ExistentialQuantification extension allows you to define datatypes
like this:

    data Stream a = forall b. MkStream b (b -> a) (b -> b)
    s_head (Stream b h t) = h b
    s_tail (Stream b h t) = Stream (t b) h t

A Stream has a seed of SOME type, and functions which get the current
element or update the seed.

The type of MkStream is a rank-1 type:

    MkStream :: forall a b. b -> (b -> a) -> (b -> b) -> Stream a

(Normally, the "forall a b." would be implicit, because it's always at
the beginning for rank-1 types, and Haskell can distinguish type
variables from constructors.)

A "destructor" for Stream would have a rank-2 type:

    unMkStream :: forall a w. (forall b. b -> (b -> a) -> (b -> b) ->
w) -> Stream a -> w
    unMkStream k (Stream b h t) = k b h t

(The destructor illustrates how pattern-matching works. "either" and
"maybe" are examples of destructors in the Prelude.)

Functions which look inside the MkStream constructor have to be
defined for ALL possible seed types.

--

PolymorphicComponents (a.k.a. universal quantification) lets you use
rank 1 values as components of a datatype.

    data Iterator f = MkIterator
        { it_head :: forall a. f a -> a
        , it_tail :: forall a. f a -> f a
        }

An Iterator has two functions that return the head or tail of a
collection, which may have ANY type.

Now the constructor is rank 2:

    MkIterator :: forall f. (forall a. f a -> a) -> (forall a. f a ->
f a) -> Iterator f

The field selectors are rank 1:

    it_head :: forall f a. Iterator f -> f a -> a
    it_tail :: forall f a. Iterator f -> f a -> f a

And the destructor is rank 3:

    unMkIterator :: forall f w. ((forall a. f a -> a) -> (forall a. f
a -> f a) -> w) -> Iterator f -> w

It's rank 3, because the type "forall a. f a -> a" is rank 1, and it's
the argument to a function (which is rank 2), that is the argument to
another function (which is rank 3).

Because Hugs only supports rank-2 polymorphism, it won't accept
unMkIterator. GHC's rank-N polymorphism means that it will, because it
will accept types of any rank.

Hope this helps.