[Haskell] Rank-N types vs existential types

[Andreas Rossberg]

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