Derek Elkins <[EMAIL PROTECTED]> writes: > On Thu, 9 Oct 2003 19:13:48 -0700 (PDT) > [EMAIL PROTECTED] wrote: > > ... > > It seems that > > (g.f) :: i -> o > > is equivalent to stating > > exists c. f:: (i->c) ^ g::(c->o) > > or, in the Haskell type language > > data P i o = forall c. P (i->c) (c->o) > > P f g > > As always, the wiki has some remarks about this, > http://www.haskell.org/hawiki/ExistentialTypes.
Interestingly, the Haskell Wiki page has an example very similar to the one which prompted my questioning in the first place. I've been reading the paper by John Hughes and Doaitse Swierstra from this year's ICFP, "Polish Parsers, step by step" (or words to that effect). There they use a type pretty similar to this one from the Wiki page: > data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b) I've been trying to convince myself that we really need the existential types here. Q: What can we do with a value of type (b -> a)? A: Apply it to a "b". Q: What can we do with a value of type b? A: Apply (b -> a) to it. Now (Expr a) is really two things: * A structural representation of a term * A fancy representation of a set of function applications So there are really two functions of interest: > getValue :: Expr a -> a -- polymorphic recursion! Signature required! > getValue (Val a) = a > getValue (Apply f b) = getValue f $ getValue b > getStructure :: Expr a -> Expr b -- Strip out the Vals > getStructure (Val a) = Val undefined > getStructure (Apply f b) = Apply (getStructure f) (getStructure b) Using this observation, we might redefine Expr in a number of ways which avoid the existential type: > -- First, a version in which the rightmost Val is the result of getValue. > data Expr' a = Val' a | Apply' (Expr' ()) (Expr' a) > > val = Val > > apply :: Expr' (a -> b) -> Expr' b -> Expr' a > apply f b = Apply' (getStructure' f) (applyVal (getValue' f) b) > -- in practice you'd want a getStructureAndValue here so that > -- this can't leak space. But the original data structure had > -- the same issue. > > applyVal :: (a -> b) -> Expr a -> Expr b > applyVal f (Val' v) = f v > applyVal f (Apply' g b) = Apply' g (applyVal f b) > > getValue' :: Expr' a -> a > getValue' (Val' v) = v > getValue' (Apply f v) = getValue' v > > getStructure' :: Expr a -> Expr b > getStructure' e = applyVal (const undefined) e I've sort-of convinced myself that you could use this trick on the data structure in the paper. > -- Similarly, we might just keep value and structure separate > data Expr'' a = Expr'' a Structure > data Structure = Value | Application Structure Structure > > val' a = Expr'' a Value > > apply :: Expr'' (a -> b) -> Expr'' b -> Expr'' a > apply (Expr'' f s) (Expr'' b t) = Expr'' (f b) (Application s t) > > getValue'' (Expr'' v _) = v > getStructure'' (Expr'' _ s) = s I guess I'm now back to my original puzzlement: do we *ever* need existential types given laziness and higher-order functions? Or are they just a convenience? I'm crystallizing a bunch of hunches here. That's made this conversation incredibly useful for me. Thanks to all so far. -Jan-Willem Maessen [EMAIL PROTECTED] _______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
