[Haskell] Rank-N types vs existential types
rossberg at ps.uni-sb.de
Wed Apr 27 07:35:04 EDT 2005
Andre Pang wrote:
>> data RankN = RankNEq (forall a. Eq a => a -> a -> Bool)
>> | RankNOrd (forall a. Ord a => a -> a -> Bool)
>> data Exists = forall a. Eq a => ExistsEq (a -> a -> Bool)
>> | forall a. Ord a => ExistsOrd (a -> a -> Bool)
> So, the RankN type uses rank-2 polymorphism to "hide" the expression
> inside the type, whereas the Exists type uses existentially quantified
> types instead. The two seem pretty equivalent to me, since the data
> constructors have the same type. However, I can't help but feel that
> I'm missing something fundamental about a difference between them. Are
> the two completely isomorphic? Is there some advantage or disadvantage
> to using one over the other?
They don't have the same type. The types are
RankNEq :: (forall a.Eq a => a->a->Bool) -> RankN
ExistsEq :: forall a.Eq a => (a->a->Bool -> Exists)
These are quite different beasts.
The difference really shows up when you *use* (deconstruct) them:
g (RankNEq f) = (f 4 5, f True False)
This allows the embedded function to be used polymorphically. But:
h (ExistsEq f) = ???
Here, you cannot use f at all (well, except with undefined). The type is
not polymorphic in "a" on the RHS, it is abstract! You'd need to
encapsulate a value of the same type (or a constructing function) as
well to this type useful.
Andreas Rossberg, rossberg at ps.uni-sb.de
Let's get rid of those possible thingies! -- TB
More information about the Haskell