Sorry to beat a dead horse (this discussion originated on the GHC bugs
list), but after trying to program up some more monad transformers, I'm
getting concerned about the expressivity of the type system with regards to
the multi-parameter type classes.  To reiterate, the examples I'm working
with are the ones from the modular interpreters paper[1].

After bringing up a related problem earlier, Simon pointed out a simple
solution, but it seems to lead to other problems later on.  The monad
transformer class

-- "MonadT" looks too much like "Monad" so I call it "Transform"
class (Monad m, Monad (t m)) => Transform t m where
  lift :: m a -> (t m) a

can't be represented directly in GHC because the second assumption violates
the rule that contexts can only constrain type variables.  The solution for
the case I had mentioned was simply to drop the assumption, since it was
redundant in that example.  But it's not redundant in some other cases, and
there is also a problem with overlapping.

For example, if you try

instance (ErrMonad m err, Transform t m) => ErrMonad (t m) err where
  err = lift . err

you will find that not only is the necessary context Monad (t m)
underivable, but also that this definition overlaps with an earlier instance
declaration:

instance (Monad m) => ErrMonad (Err err m) err where
  ...

The latter problem looks solvable using the
promised -fallow-overlapping-instances option, since the overlapping is a
specialization, but clearly it's not possible to just add Monad (t m) to the
context here.  These same problems look like they will appear for other
liftings.

It looks to me like the restriction that contexts can only constrain type
variables will force you to define many more instances than would be
necessary using Gofer's type system.  This is rather disappointing for me; I
can see how "variable monads" and container types fit well into the present
system, but, since [1] is to my knowledge the most extensive example of
using MPTC with monads, I assumed that the type system was designed with it
in mind.

Maybe I'm wrong, and someone more knowledgeable than I can refactor the
transformer definitions in a way that avoids these problems.  If so, I would
be grateful---and I think others will also benefit---if they would write up
a module for GHC that showed how to implement the transformers mentioned in
the paper.  For reference, I'm attaching the portion I've done so far.

[1] Sheng Liang, Paul Hudak and Mark Jones.  Monad Transformers and Modular
Interpreters.  In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, San Francisco, CA, January
1995.
URL: http://www.cs.nott.ac.uk:80/Department/Staff/mpj/modinterp.html

---
> {-# OPTIONS -fglasgow-exts #-}
> module Feature
> where

\section{Monad transformers}

> class (Monad m) => Transform t m where
>   lift :: m a -> (t m) a

\subsection{Environments}

> class (Monad m) => EnvMonad m env where
>   inEnv  :: env -> m a -> m a
>   getEnv :: m env

> newtype Env env m a = Env (env -> m a)
> unEnv (Env f) = f
>
> instance (Monad m) => Monad (Env env m) where
>   return x = Env $ const (return x)
>   (Env m) >>= f = Env $ \env -> m env >>= \a -> (unEnv $ f a) env

> instance (Monad m) => Transform (Env env) m where
>   lift m  = Env $ const m

To lift an action through an environment monad, simply ignore the
environment.

\subsection{State}

> class (Monad m) => StateMonad m state where
>   modify :: (state -> state) -> m state

> newtype State s m a = State (s -> m (s,a))
> unState (State f) = f
>
> instance (Monad m) => Monad (State s m) where
>   return x = State $ \s -> return (s,x)
>   (State m) >>= f = State $ \s -> m s >>= \(s',a) -> (unState $ f a) s

> instance (Monad m) => Transform (State s) m where
>   -- lift :: m a -> State s m a
>   lift action = State $ \s -> action >>= \a -> return (s,a)

To lift an action through a state monad, pass the state through unchanged.

\subsection{Errors}

> class (Monad m) => ErrMonad m err where
>   err :: err -> m a

> newtype Err err m a = Err (m (Either err a))
> unErr (Err m) = m
>
> instance (Monad m) => Monad (Err err m) where
>   return x = Err $ return (Right x)
>   -- ErrorT m err a -> (a -> ErrorT m err b) -> ErrorT m err b
>   (Err action) >>= f = Err $ action >>= \a ->
>     case a of
>       Right x -> unErr (f x)
> Left e -> return (Left e)
>
> instance (Monad m) => ErrMonad (Err err m) err where
>   err e = Err $ return (Left e)

> instance (Monad m) => Transform (Err err) m where
>   -- lift :: m a -> Err err m a
>   lift action = Err $ action >>= \a -> return (Right a)

Define the result of running an action lifted through the error monad
to not raise an error.

\subsection{Continuations}

> class (Monad m) => ContMonad m where
>   callcc :: ((a -> m b) -> m a) -> m a

> newtype Cont ans m a = Cont ((a -> m ans) -> m ans)
> unCont (Cont f) = f
>
> instance (Monad m) => Monad (Cont ans m) where
>   return x    = Cont $ \k -> k x
>   -- Cont ans m a -> (a -> Cont ans m b) -> Cont ans m b
>   -- m :: (a -> m ans) -> m ans
>   -- f :: a -> Cont ans m b
>   -- f a :: Cont ans m b
>   -- (unCont $ f a) :: (b -> m ans) -> m ans
>   (Cont m) >>= f = Cont $ \k -> m (\a -> (unCont $ f a) k)

> instance (Monad m) => Transform (Cont ans) m where
>   -- lift :: m a -> Cont ans m a
>   lift action = Cont $ \k -> action >>= k

To lift an action through the continuation monad, run the action and pass
the result to the current continuation.

\subsection{Non-determinism}

> class (Monad m) => ListMonad m where
>   merge :: [m a] -> m a
>
> instance ListMonad [] where
>   merge = concat

\subsection{Liftings}

> instance (ErrMonad m err, Transform t m) => ErrMonad (t m) err where
>   err = lift . err


Reply via email to