On Sat, Oct 16, 2004 at 10:19:14AM +0900, Koji Nakahara wrote:

On Fri, 15 Oct 2004 19:55:02 -0400 Andrew Pimlott wrote:

...

data Foo = forall t. (MonadTrans t) => Foo ((Monad m, Monad (t m)) => t m a -> m a) -- run ((Monad m, Monad (t m)) => t m Int) -- op

prog :: Foo -> IO Int prog (Foo run op) = run $ do lift $ putStrLn "Running prog" op

ghci gives the error

Could not deduce (Monad (t IO)) from the context (MonadTrans t) arising from use of `op' at try.hs:22

Your prog leaks m (= IO) out of Foo. I guess you mean:

...

data Foo m = forall t. (MonadTrans t, Monad (t m)) => Foo (forall a. t m a -> m a) (t m Int)

prog :: Foo IO -> IO Int prog (Foo run op) = run $ do lift $ putStrLn "Running prog" op

test = prog (Foo (flip evalStateT 0) get)

But my implementation may look like myFoo :: Int -> Foo myFoo i = Foo 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 which works for all monads, not just IO (that is the idea of using a tranformer). So I really don't want to encode that type in Foo. Andrew

On Fri, Oct 15, 2004 at 07:54:46PM -0700, oleg@pobox.com wrote:

Andrew Pimlott wrote:

...

I want values in my existential type to denote, for some monad, a monadic operation and a way to run the monad. Except, I want it mix the operation with operations in another monad, so it use a monad transformer.

I'm afraid, that phrase was a little misleading. It seems that you meant: - encapsulate one _specific_ monad transformer - to be able to apply it to _any_ (not some!) monad

Yes. I wrote that quickly (grammar mistakes too) and thought the code would make it clear. But it would have been better to make the words precise.

...

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)

Wow, very nice. Just do it in two steps! Thank you for this enlightening solution. Andrew

...

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.