[Haskell-cafe] existential type problem

[oleg at pobox.com]

> > data Bar a m = forall t. (MonadTrans t, Monad (t m)) =>
> >              Bar (t m a -> m a) (t m Int)
> > data Foo = Foo (forall a m. Monad m => Bar a m)
>
> Is it true that I cannot have a function
>
>     foo run op = Foo (Bar run op)

I guess the answer is yes and no. Let's consider the type of 'op':

  exists t. forall m. (MonadTrans t, Monad m, Monad (t m)) => t m Int

obviously, we can't write such a type expression in Haskell. There are
two work-arounds however. First, we can perform existential
instantiation: that is, replace t with some specific type (type
constructor, that is). We should also make sure that MonadTrans t and
Monad (t m) constraints are satisfied after such a replacement (the
typechecker will complain otherwise). So, we come to one known
solution:

> > myFoo :: Int -> Foo
> > myFoo i = Foo (Bar run op) where
> >   run :: Monad m => StateT Int m a -> m a
> >   run prog  = do  (a, s) <- runStateT prog i
> >                 return a
> >   op :: Monad m => StateT Int m Int
> >   op        = get

Here, we replaced t with the specific type constructor StateT.

Another way of handling the above type for 't' -- another way of
getting rid of the existential quantification -- is to negate the type
expression. In other words, make that 'op' an argument of a function,
and be sure that 't' doesn't show up in the result. But that's what our
'Bar' already does:

*P> :t Bar
Bar :: forall m a t.
       (Monad (t m), MonadTrans t) =>
       (t m a -> m a) -> t m Int -> Bar a m

We note that t is not a function of m, so the order of quantification
will indeed be "exists t. forall m. ...". That's how we recover the
two-step solution, with Foo and Bar.