[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