[Haskell-cafe] Existencial Types

[Ryan Ingram]

On Tue, Dec 1, 2009 at 4:44 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
> 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