[Haskell-cafe] existential type problem
oleg at pobox.com
oleg at pobox.com
Sat Oct 23 01:08:25 EDT 2004
> > 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.
More information about the Haskell-Cafe
mailing list