Rank-N types vs existential types
Hi all, Let's say I have the following two data types:
{-# OPTIONS_GHC -fglasgow-exts #-}
module RankNVsExists where
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? -- % Andre Pang : trust.in.love.to.save <http://www.algorithm.com.au/>
RankN and Exists are completelly different. The types of RankNEq and ExistsEq constructors are: RankNEq :: (forall a. Eq a => a -> a -> Bool) -> RankN ExistsEq :: forall a. Eq a => (a -> a -> Bool) -> Exists i.e. RankNEq requires one argument, which is a polymorfic function that have to be applied to Eq dictonary. ExistsEq have two arguments: an Eq dictonary and function of type (a -> a -> Bool). Cheers, Krasimir On 4/27/05, Andre Pang <ozone@algorithm.com.au> wrote:
Hi all,
Let's say I have the following two data types:
{-# OPTIONS_GHC -fglasgow-exts #-}
module RankNVsExists where
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?
-- % Andre Pang : trust.in.love.to.save <http://www.algorithm.com.au/>
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On 27/04/2005, at 9:26 PM, Krasimir Angelov wrote:
RankN and Exists are completelly different. The types of RankNEq and ExistsEq constructors are:
RankNEq :: (forall a. Eq a => a -> a -> Bool) -> RankN ExistsEq :: forall a. Eq a => (a -> a -> Bool) -> Exists
i.e. RankNEq requires one argument, which is a polymorfic function that have to be applied to Eq dictonary. ExistsEq have two arguments: an Eq dictonary and function of type (a -> a -> Bool).
Thanks Krasimir and Tomasz for that clarification. Unfortunately, I'm still a bit confused :). Krasimir, from what you say, this sounds like a big difference in implementation, but from a Haskell (non-type-wizard) user's point of view, is there a practical difference between the two? I can't think of a situation where rank-N/existentials couldn't be substituted for the other ... -- % Andre Pang : trust.in.love.to.save <http://www.algorithm.com.au/>
Yes. There is a significant difference in both the internal representation and the high level representation. ExistsEq is a structure with two internal fields the dictionary and the function, while the RankNEq has only one field. As Andreas Rossberg noted ExistsEq is useless without extra fields. Here is an example which might be more useful: data Exists = Eq a => Exists (a -> a) a a next :: Exists -> Maybe Exists next (Exists f x y) | x == y = Nothing | otherwise = Just (Exists f (f x) y) Note that the only functions which I can apply over type 'a' are (==) and f. Cheers, Krasimir On 4/27/05, Andre Pang <ozone@algorithm.com.au> wrote:
On 27/04/2005, at 9:26 PM, Krasimir Angelov wrote:
RankN and Exists are completelly different. The types of RankNEq and ExistsEq constructors are:
RankNEq :: (forall a. Eq a => a -> a -> Bool) -> RankN ExistsEq :: forall a. Eq a => (a -> a -> Bool) -> Exists
i.e. RankNEq requires one argument, which is a polymorfic function that have to be applied to Eq dictonary. ExistsEq have two arguments: an Eq dictonary and function of type (a -> a -> Bool).
Thanks Krasimir and Tomasz for that clarification. Unfortunately, I'm still a bit confused :). Krasimir, from what you say, this sounds like a big difference in implementation, but from a Haskell (non-type-wizard) user's point of view, is there a practical difference between the two? I can't think of a situation where rank-N/existentials couldn't be substituted for the other ...
-- % Andre Pang : trust.in.love.to.save <http://www.algorithm.com.au/>
On Wed, Apr 27, 2005 at 09:16:16PM +1000, 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)
The two seem pretty equivalent to me, since the data constructors have the same type.
They don't: ExistsEq :: (Eq a) => (a -> a -> Bool) -> Exists RankNEq :: (forall a. (Eq a) => a -> a -> Bool) -> RankN Best regards Tomasz
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@ps.uni-sb.de Let's get rid of those possible thingies! -- TB
On 27/04/2005, at 9:35 PM, Andreas Rossberg wrote:
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.
Ah, OK! That's quite enlightening. Thanks Andreas, Krasimir, and Tomasz for all your replies. -- % Andre Pang : trust.in.love.to.save <http://www.algorithm.com.au/>
participants (4)
-
Andre Pang -
Andreas Rossberg -
Krasimir Angelov -
Tomasz Zielonka