[Haskell-cafe] Type system madness

David Menendez zednenem at psualum.com
Mon Jul 9 19:15:36 EDT 2007

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.

More information about the Haskell-Cafe mailing list