On Tue, Dec 1, 2009 at 4:44 PM, Luke Palmer
Existential types only buy you power when the quantified variable appears more than once on the right hand side, for example: forall a. Num a => (a,a). But even those can usually be factored out into more direct representations (I seem to recall Oleg has a proof that they always can, actually).
You are probably right that there is an encoding that doesn't use existentials, but I've found they can be very useful in a few situations, such as: data Step s a = Done | Yield s a | Skip s data Stream a = forall s. Stream s (s -> Step s a) Here the type of the stream state is encapsulated and not accessible to the outside world, but it can still get some values of that type via the result of the Step function. data Expr a where ... App :: Expr (a -> b) -> Expr a -> Expr b Here we quantify over the type of the argument "a"; we just know that we have an expression of that type and an expression of the function type it wants. -- ryan