On 7/9/07, Andrew Coppin <[EMAIL PROTECTED]> 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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to