diff --git a/monadLib.cabal b/monadLib.cabal
--- a/monadLib.cabal
+++ b/monadLib.cabal
@@ -1,17 +1,18 @@
 Name:           monadLib
-Version:        3.3.0
+Version:        3.4.4
 License:        BSD3
 License-file:   LICENSE
 Author:         Iavor S. Diatchki
 Maintainer:     diatchki@galois.com
-Homepage:       http://www.galois.com/~diatchki/monadLib
+Homepage:       http://www.purely-functional.net/monadLib
 Category:       Monads
 Synopsis:       A collection of monad transformers.
 Description:    A collection of monad transformers.
 hs-source-dirs: src
 Build-Depends:  base
+Build-type:     Simple
 Extra-source-files: LICENSE, README, CHANGES
-Exposed-modules: MonadLib, Monads
+Exposed-modules: MonadLib, MonadLib.Monads, MonadLib.Derive
 Extensions:
   MultiParamTypeClasses, FunctionalDependencies, Rank2Types
 GHC-options:    -O2 -W -fallow-undecidable-instances
diff --git a/src/MonadLib.hs b/src/MonadLib.hs
--- a/src/MonadLib.hs
+++ b/src/MonadLib.hs
@@ -5,7 +5,12 @@
 module MonadLib (
   -- * Types
   -- $Types
-  Id, Lift, IdT, ReaderT, WriterT, StateT, ExceptionT, ContT,
+  Id, Lift, IdT, ReaderT, WriterT,
+  StateT,
+  ExceptionT,
+  -- 
+  -- $WriterM_ExceptionT
+  ChoiceT, ContT,
 
   -- * Lifting
   -- $Lifting
@@ -21,31 +26,30 @@
   -- ** Eliminating Effects
   -- $Execution
   runId, runLift,
-  runIdT, runReaderT, runWriterT, runStateT, runExceptionT, runContT,
+  runIdT, runReaderT, runWriterT,
+  runStateT, runExceptionT, runContT,
+  runChoiceT, findOne, findAll,
 
   -- ** Nested Execution
   -- $Nested_Exec
   RunReaderM(..), RunWriterM(..), RunExceptionM(..),
 
-  -- * Deriving functions
-  Iso(..), derive_fmap, derive_return, derive_bind, derive_fail, derive_mfix,
-  derive_ask, derive_put, derive_get, derive_set, derive_raise, derive_callCC,
-  derive_local, derive_collect, derive_try,
-  derive_lift, derive_inBase,
-
   -- * Miscellaneous
   version,
   module Control.Monad
 ) where
 
+
+import Control.Applicative
 import Control.Monad
 import Control.Monad.Fix
+import qualified Control.Exception as IO (throwIO,try,Exception)
 import Data.Monoid
 import Prelude hiding (Ordering(..))
 
 -- | The current version of the library.
 version :: (Int,Int,Int)
-version = (3,3,0)
+version = (3,4,4)
 
 
 -- $Types
@@ -60,25 +64,34 @@
 -- | Computation with no effects (strict).
 data Lift a               = L a
 
--- | Add nothing.  Useful as a placeholder.
+-- | Adds no new features.  Useful as a placeholder.
 newtype IdT m a           = IT (m a)
 
--- | Add support for propagating a context.
-newtype ReaderT    i m a  = R (i -> m a)
+-- | Add support for propagating a context of type @i@.
+newtype ReaderT i m a     = R (i -> m a)
 
--- | Add support for collecting values.
-newtype WriterT    i m a  = W (m (a,i))
+-- | Add support for collecting values of type @i@.
+-- The type @i@ should be a monoid, whose unit is used to represent
+-- a lack of a value, and whose binary operation is used to combine
+-- multiple values.
+-- This transformer is strict in its output component.
+newtype WriterT i m a = W { unW :: m (P a i) }
+data P a i = P a !i
 
--- | Add support for threading state.
+-- | Add support for threading state of type @i@.
 newtype StateT     i m a  = S (i -> m (a,i))
 
--- | Add support for exceptions.
+-- | Add support for exceptions of type @i@.
 newtype ExceptionT i m a  = X (m (Either i a))
 
--- | Add support for jumps.
-newtype ContT      i m a  = C ((a -> m i) -> m i)
-
+-- | Add support for multiple answers.
+data ChoiceT m a          = NoAnswer
+                          | Answer a
+                          | Choice (ChoiceT m a) (ChoiceT m a)
+                          | ChoiceEff (m (ChoiceT m a))
 
+-- | Add support for continuations within a prompt of type @i@.
+newtype ContT i m a  = C ((a -> m i) -> m i)
 
 -- $Execution
 --
@@ -109,8 +122,9 @@
 
 -- | Execute a writer computation.
 -- Returns the result and the collected output.
-runWriterT    :: WriterT i m a -> m (a,i)
-runWriterT (W m) = m
+runWriterT :: (Monad m) => WriterT i m a -> m (a,i)
+runWriterT (W m) = liftM to_pair m
+  where to_pair ~(P a w) = (a,w)
 
 -- | Execute a stateful computation in the given initial state.
 -- The second component of the result is the final state.
@@ -123,6 +137,34 @@
 runExceptionT :: ExceptionT i m a -> m (Either i a)
 runExceptionT (X m) = m
 
+-- | Execute a computation that may return multiple answers.
+-- The resulting computation returns 'Nothing'
+-- if no answers were found, or @Just (answer,new_comp)@,
+-- where @answer@ is an answer, and @new_comp@ is a computation
+-- that may produce more answers.
+-- The search is depth-first and left-biased with respect to the
+-- 'mplus' operation.
+runChoiceT :: (Monad m) => ChoiceT m a -> m (Maybe (a,ChoiceT m a))
+runChoiceT (Answer a)     = return (Just (a,NoAnswer))
+runChoiceT NoAnswer       = return Nothing
+runChoiceT (Choice l r)   = do x <- runChoiceT l
+                               case x of
+                                 Nothing      -> runChoiceT r
+                                 Just (a,l1)  -> return (Just (a,Choice l1 r))
+runChoiceT (ChoiceEff m)  = runChoiceT =<< m
+
+-- | Execute a computation that may return multiple answers,
+-- returning at most one answer.
+findOne :: (Monad m) => ChoiceT m a -> m (Maybe a)
+findOne m = fmap fst `liftM` runChoiceT m
+
+-- | Executie a computation that may return multiple answers,
+-- collecting all possible answers.
+findAll :: (Monad m) => ChoiceT m a -> m [a]
+findAll m = all_res =<< runChoiceT m
+  where all_res Nothing       = return []
+        all_res (Just (a,as)) = (a:) `liftM` findAll as
+
 -- | Execute a computation with the given continuation.
 runContT      :: (a -> m i) -> ContT i m a -> m i
 runContT i (C m) = m i
@@ -137,22 +179,65 @@
 -- the new effect but can be combined with other operations that
 -- utilize the effect.
 
+
+-- Notes:
+--   * It is interesting to note that these use something the resembles
+--     the non-transformer 'return's.
+--   * These are more general then the lift in the MonadT class because
+--     most of them can lift arbitrary functors (some, even arbitrary type ctrs)
+lift_IdT m          = IT m
+lift_ReaderT m      = R (\_ -> m)
+lift_StateT f m     = S (\s -> f (\a -> (a,s)) m)
+lift_WriterT f m    = W (f (\a -> P a mempty) m)
+lift_ExceptionT f m = X (f Right m)
+lift_ChoiceT f m    = ChoiceEff (f Answer m)
+lift_ContT f m      = C (f m)
+
 class MonadT t where
   -- | Promote a computation from the underlying monad.
   lift :: (Monad m) => m a -> t m a
 
--- It is interesting to note that these use something the resembles
--- the non-transformer 'return's.
+instance MonadT IdT            where lift = lift_IdT
+instance MonadT (ReaderT    i) where lift = lift_ReaderT
+instance MonadT (StateT     i) where lift = lift_StateT liftM
+instance (Monoid i)
+      => MonadT (WriterT i)    where lift = lift_WriterT liftM
+instance MonadT (ExceptionT i) where lift = lift_ExceptionT liftM
+instance MonadT ChoiceT        where lift = lift_ChoiceT liftM
+instance MonadT (ContT      i) where lift = lift_ContT (>>=)
 
-instance MonadT IdT            where lift m = IT m
-instance MonadT (ReaderT    i) where lift m = R (\_ -> m)
-instance MonadT (StateT     i) where lift m = S (\s -> liftM (\a -> (a,s)) m)
-instance (Monoid i) =>
-         MonadT (WriterT    i) where lift m = W (liftM (\a -> (a,mempty)) m)
-instance MonadT (ExceptionT i) where lift m = X (liftM Right m)
-instance MonadT (ContT      i) where lift m = C (m >>=)
 
+-- Definitions for some of the methods that are the same for all transformers
 
+t_inBase   :: (MonadT t, BaseM m n) => n a -> t m a
+t_inBase m  = lift (inBase m)
+
+t_return   :: (MonadT t, Monad m) => a -> t m a
+t_return x  = lift (return x)
+
+t_fail     :: (MonadT t, Monad m) => String -> t m a
+t_fail x    = lift (fail x)
+
+t_mzero    :: (MonadT t, MonadPlus m) => t m a
+t_mzero     = lift mzero
+
+t_ask      :: (MonadT t, ReaderM m i) => t m i
+t_ask       = lift ask
+
+t_put      :: (MonadT t, WriterM m i) => i -> t m ()
+t_put x     = lift (put x)
+
+t_get      :: (MonadT t, StateM m i) => t m i
+t_get       = lift get
+
+t_set      :: (MonadT t, StateM m i) => i -> t m ()
+t_set i     = lift (set i)
+
+t_raise    :: (MonadT t, ExceptionM m i) => i -> t m a
+t_raise i   = lift (raise i)
+--------------------------------------------------------------------------------
+
+
 class (Monad m, Monad n) => BaseM m n | m -> n where
   -- | Promote a computation from the base monad.
   inBase :: n a -> m a
@@ -163,83 +248,126 @@
 instance BaseM Id Id        where inBase = id
 instance BaseM Lift Lift    where inBase = id
 
-instance (BaseM m n) => BaseM (IdT          m) n where inBase = lift . inBase
-instance (BaseM m n) => BaseM (ReaderT    i m) n where inBase = lift . inBase
-instance (BaseM m n) => BaseM (StateT     i m) n where inBase = lift . inBase
-instance (BaseM m n,Monoid i) =>
-                        BaseM (WriterT    i m) n where inBase = lift . inBase
-instance (BaseM m n) => BaseM (ExceptionT i m) n where inBase = lift . inBase
-instance (BaseM m n) => BaseM (ContT      i m) n where inBase = lift . inBase
 
+instance (BaseM m n) => BaseM (IdT          m) n where inBase = t_inBase
+instance (BaseM m n) => BaseM (ReaderT    i m) n where inBase = t_inBase
+instance (BaseM m n) => BaseM (StateT     i m) n where inBase = t_inBase
+instance (BaseM m n,Monoid i)
+                     => BaseM (WriterT i m) n    where inBase = t_inBase
+instance (BaseM m n) => BaseM (ExceptionT i m) n where inBase = t_inBase
+instance (BaseM m n) => BaseM (ChoiceT      m) n where inBase = t_inBase
+instance (BaseM m n) => BaseM (ContT      i m) n where inBase = t_inBase
 
+
 instance Monad Id where
   return x = I x
   fail x   = error x
   m >>= k  = k (runId m)
 
-
 instance Monad Lift where
   return x  = L x
   fail x    = error x
-  L x >>= k = k x
+  L x >>= k = k x     -- Note: the pattern is important here
+                      -- because it makes things strict
 
--- For the monad transformers, the definition of 'return'
--- is completely determined by the 'lift' operations.
 
--- None of the transformers make essential use of the 'fail' method.
--- Instead they delegate its behavior to the underlying monad.
+-- Note: None of the transformers make essential use of the 'fail' method.
+-- Instead, they delegate its behavior to the underlying monad.
 
 instance (Monad m) => Monad (IdT m) where
-  return x    = lift (return x)
-  fail x      = lift (fail x)
-  m >>= k     = IT (runIdT m >>= (runIdT . k))
+  return  = t_return
+  fail    = t_fail
+  m >>= k = IT (runIdT m >>= (runIdT . k))
 
 instance (Monad m) => Monad (ReaderT i m) where
-  return x = lift (return x)
-  fail x   = lift (fail x)
-  m >>= k  = R (\r -> runReaderT r m >>= \a -> runReaderT r (k a))
+  return  = t_return
+  fail    = t_fail
+  m >>= k = R (\r -> runReaderT r m >>= \a -> runReaderT r (k a))
 
 instance (Monad m) => Monad (StateT i m) where
-  return x = lift (return x)
-  fail x   = lift (fail x)
-  m >>= k  = S (\s -> runStateT s m >>= \ ~(a,s') -> runStateT s' (k a))
+  return  = t_return
+  fail    = t_fail
+  m >>= k = S (\s -> runStateT s m >>= \ ~(a,s') -> runStateT s' (k a))
 
 instance (Monad m,Monoid i) => Monad (WriterT i m) where
-  return x = lift (return x)
-  fail x   = lift (fail x)
-  m >>= k  = W $ runWriterT m     >>= \ ~(a,w1) ->
-                 runWriterT (k a) >>= \ ~(b,w2) ->
-                 return (b,mappend w1 w2)
+  return  = t_return
+  fail    = t_fail
+  m >>= k = W $ unW m     >>= \ ~(P a w1) ->
+                unW (k a) >>= \ ~(P b w2) ->
+                return (P b (mappend w1 w2))
 
 instance (Monad m) => Monad (ExceptionT i m) where
-  return x = lift (return x)
-  fail x   = lift (fail x)
-  m >>= k  = X $ runExceptionT m >>= \a ->
-                 case a of
-                   Left x  -> return (Left x)
-                   Right a -> runExceptionT (k a)
+  return  = t_return
+  fail    = t_fail
+  m >>= k = X $ runExceptionT m >>= \e ->
+                case e of
+                  Left x  -> return (Left x)
+                  Right a -> runExceptionT (k a)
 
+instance (Monad m) => Monad (ChoiceT m) where
+  return x  = Answer x
+  fail x    = lift (fail x)
+
+  Answer a  >>= k     = k a
+  NoAnswer >>= _      = NoAnswer
+  Choice m1 m2 >>= k  = Choice (m1 >>= k) (m2 >>= k)
+  ChoiceEff m >>= k   = ChoiceEff (liftM (>>= k) m)
+
 instance (Monad m) => Monad (ContT i m) where
-  return x = lift (return x)
-  fail x   = lift (fail x)
-  m >>= k  = C $ \c -> runContT (\a -> runContT c (k a)) m
+  return  = t_return
+  fail    = t_fail
+  m >>= k = C $ \c -> runContT (\a -> runContT c (k a)) m
 
 instance                       Functor Id               where fmap = liftM
 instance                       Functor Lift             where fmap = liftM
 instance (Monad m)          => Functor (IdT          m) where fmap = liftM
 instance (Monad m)          => Functor (ReaderT    i m) where fmap = liftM
 instance (Monad m)          => Functor (StateT     i m) where fmap = liftM
-instance (Monad m,Monoid i) => Functor (WriterT    i m) where fmap = liftM
+instance (Monad m,Monoid i) => Functor (WriterT i m)    where fmap = liftM
 instance (Monad m)          => Functor (ExceptionT i m) where fmap = liftM
+instance (Monad m)          => Functor (ChoiceT      m) where fmap = liftM
 instance (Monad m)          => Functor (ContT      i m) where fmap = liftM
 
+-- Applicative support ---------------------------------------------------------
 
+-- NOTE: It may be possible to make these more general
+-- (i.e., have Applicative, or even Functor transformers)
+
+instance              Applicative Id            where (<*>) = ap; pure = return
+instance              Applicative Lift          where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (IdT m)       where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (ReaderT i m) where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (StateT i m)  where (<*>) = ap; pure = return
+instance (Monad m,Monoid i)
+                   => Applicative (WriterT i m) where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (ExceptionT i m)
+                                                where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (ChoiceT m)   where (<*>) = ap; pure = return
+instance (Monad m) => Applicative (ContT i m)   where (<*>) = ap; pure = return
+
+instance (MonadPlus m)
+           => Alternative (IdT m)           where (<|>) = mplus; empty = mzero
+instance (MonadPlus m)
+           => Alternative (ReaderT i m)     where (<|>) = mplus; empty = mzero
+instance (MonadPlus m)
+           => Alternative (StateT i m)      where (<|>) = mplus; empty = mzero
+instance (MonadPlus m,Monoid i)
+           => Alternative (WriterT i m)     where (<|>) = mplus; empty = mzero
+instance (MonadPlus m)
+           => Alternative (ExceptionT i m)  where (<|>) = mplus; empty = mzero
+instance (Monad m)
+           => Alternative (ChoiceT m)       where (<|>) = mplus; empty = mzero
+instance (MonadPlus m)
+           => Alternative (ContT i m)       where (<|>) = mplus; empty = mzero
+
+
+
 -- $Monadic_Value_Recursion
 --
 -- Recursion that does not duplicate side-effects.
 -- For details see Levent Erkok's dissertation.
 --
--- Monadic types built with 'ContT' do not support
+-- Monadic types built with 'ContT' and 'ChoiceT' do not support
 -- monadic value recursion.
 
 instance MonadFix Id where
@@ -258,36 +386,48 @@
   mfix f  = S $ \s -> mfix (runStateT s . f . fst)
 
 instance (MonadFix m,Monoid i) => MonadFix (WriterT i m) where
-  mfix f  = W $ mfix (runWriterT . f . fst)
+  mfix f  = W $ mfix (unW . f . val)
+    where val ~(P a _) = a
 
+-- No instance for ChoiceT
+
 instance (MonadFix m) => MonadFix (ExceptionT i m) where
   mfix f  = X $ mfix (runExceptionT . f . fromRight)
     where fromRight (Right a) = a
           fromRight _         = error "ExceptionT: mfix looped."
 
-
+-- No instance for ContT
 
 instance (MonadPlus m) => MonadPlus (IdT m) where
-  mzero               = lift mzero
+  mzero               = t_mzero
   mplus (IT m) (IT n) = IT (mplus m n)
 
 instance (MonadPlus m) => MonadPlus (ReaderT i m) where
-  mzero             = lift mzero
+  mzero             = t_mzero
   mplus (R m) (R n) = R (\r -> mplus (m r) (n r))
 
 instance (MonadPlus m) => MonadPlus (StateT i m) where
-  mzero             = lift mzero
+  mzero             = t_mzero
   mplus (S m) (S n) = S (\s -> mplus (m s) (n s))
 
 instance (MonadPlus m,Monoid i) => MonadPlus (WriterT i m) where
-  mzero             = lift mzero
+  mzero               = t_mzero
   mplus (W m) (W n) = W (mplus m n)
 
 instance (MonadPlus m) => MonadPlus (ExceptionT i m) where
-  mzero             = lift mzero
+  mzero             = t_mzero
   mplus (X m) (X n) = X (mplus m n)
 
+instance (Monad m) => MonadPlus (ChoiceT m) where
+  mzero             = NoAnswer
+  mplus m n         = Choice m n
 
+-- Alternatives share the continuation.
+instance (MonadPlus m) => MonadPlus (ContT i m) where
+  mzero             = t_mzero
+  mplus (C m) (C n) = C (\k -> m k `mplus` n k)
+
+
 -- $Effects
 --
 -- The following classes define overloaded operations
@@ -302,12 +442,13 @@
 instance (Monad m) => ReaderM (ReaderT i m) i where
   ask = R return
 
-instance (ReaderM m j) => ReaderM (IdT          m) j where ask = lift ask
+instance (ReaderM m j) => ReaderM (IdT m) j           where ask = t_ask
 instance (ReaderM m j,Monoid i)
-                       => ReaderM (WriterT    i m) j where ask = lift ask
-instance (ReaderM m j) => ReaderM (StateT     i m) j where ask = lift ask
-instance (ReaderM m j) => ReaderM (ExceptionT i m) j where ask = lift ask
-instance (ReaderM m j) => ReaderM (ContT      i m) j where ask = lift ask
+                       => ReaderM (WriterT i m) j     where ask = t_ask
+instance (ReaderM m j) => ReaderM (StateT i m) j      where ask = t_ask
+instance (ReaderM m j) => ReaderM (ExceptionT i m) j  where ask = t_ask
+instance (ReaderM m j) => ReaderM (ChoiceT m) j       where ask = t_ask
+instance (ReaderM m j) => ReaderM (ContT i m) j       where ask = t_ask
 
 
 -- | Classifies monads that can collect values of type @i@.
@@ -316,14 +457,14 @@
   put  :: i -> m ()
 
 instance (Monad m,Monoid i) => WriterM (WriterT i m) i where
-  put x = W (return ((),x))
-
-instance (WriterM m j) => WriterM (IdT          m) j where put = lift . put
-instance (WriterM m j) => WriterM (ReaderT    i m) j where put = lift . put
-instance (WriterM m j) => WriterM (StateT     i m) j where put = lift . put
-instance (WriterM m j) => WriterM (ExceptionT i m) j where put = lift . put
-instance (WriterM m j) => WriterM (ContT      i m) j where put = lift . put
+  put x = W (return (P () x))
 
+instance (WriterM m j) => WriterM (IdT          m) j where put = t_put
+instance (WriterM m j) => WriterM (ReaderT    i m) j where put = t_put
+instance (WriterM m j) => WriterM (StateT     i m) j where put = t_put
+instance (WriterM m j) => WriterM (ExceptionT i m) j where put = t_put
+instance (WriterM m j) => WriterM (ChoiceT      m) j where put = t_put
+instance (WriterM m j) => WriterM (ContT      i m) j where put = t_put
 
 -- | Classifies monads that propagate a state component of type @i@.
 class (Monad m) => StateM m i | m -> i where
@@ -337,40 +478,41 @@
   set s = S (\_ -> return ((),s))
 
 instance (StateM m j) => StateM (IdT m) j where
-  get = lift get
-  set = lift . set
+  get = t_get; set = t_set
 instance (StateM m j) => StateM (ReaderT i m) j where
-  get = lift get
-  set = lift . set
+  get = t_get; set = t_set
 instance (StateM m j,Monoid i) => StateM (WriterT i m) j where
-  get = lift get
-  set = lift . set
+  get = t_get; set = t_set
 instance (StateM m j) => StateM (ExceptionT i m) j where
-  get = lift get
-  set = lift . set
+  get = t_get; set = t_set
+instance (StateM m j) => StateM (ChoiceT m) j where
+  get = t_get; set = t_set
 instance (StateM m j) => StateM (ContT i m) j where
-  get = lift get
-  set = lift . set
-
+  get = t_get; set = t_set
 
 -- | Classifies monads that support raising exceptions of type @i@.
 class (Monad m) => ExceptionM m i | m -> i where
   -- | Raise an exception.
   raise :: i -> m a
 
+instance ExceptionM IO IO.Exception where
+  raise = IO.throwIO
+
 instance (Monad m) => ExceptionM (ExceptionT i m) i where
   raise x = X (return (Left x))
 
 instance (ExceptionM m j) => ExceptionM (IdT m) j where
-  raise = lift . raise
+  raise = t_raise
 instance (ExceptionM m j) => ExceptionM (ReaderT i m) j where
-  raise = lift . raise
+  raise = t_raise
 instance (ExceptionM m j,Monoid i) => ExceptionM (WriterT i m) j where
-  raise = lift . raise
+  raise = t_raise
 instance (ExceptionM m j) => ExceptionM (StateT  i m) j where
-  raise = lift . raise
+  raise = t_raise
+instance (ExceptionM m j) => ExceptionM (ChoiceT   m) j where
+  raise = t_raise
 instance (ExceptionM m j) => ExceptionM (ContT   i m) j where
-  raise = lift . raise
+  raise = t_raise
 
 
 -- The following instances differ from the others because the
@@ -391,11 +533,15 @@
   callCC f = S $ \s -> callCC $ \k -> runStateT s $ f $ \a -> lift $ k (a,s)
 
 instance (ContM m,Monoid i) => ContM (WriterT i m) where
-  callCC f = W $ callCC $ \k -> runWriterT $ f $ \a -> lift $ k (a,mempty)
+  callCC f = W $ callCC $ \k -> unW $ f $ \a -> lift $ k (P a mempty)
 
 instance (ContM m) => ContM (ExceptionT i m) where
   callCC f = X $ callCC $ \k -> runExceptionT $ f $ \a -> lift $ k $ Right a
 
+instance (ContM m) => ContM (ChoiceT m) where
+  callCC f = ChoiceEff $ callCC $ \k -> return $ f $ \a -> lift $ k $ Answer a
+    -- ??? What does this do ???
+
 instance (Monad m) => ContM (ContT i m) where
   callCC f = C $ \k -> runContT k $ f $ \a -> C $ \_ -> k a
 
@@ -411,8 +557,9 @@
 -- | Classifies monads that support changing the context for a
 -- sub-computation.
 class (ReaderM m i) => RunReaderM m i | m -> i where
-  -- | Change the context for the duration of a computation.
+  -- | Change the context for the duration of a sub-computation.
   local        :: i -> m a -> m a
+  -- prop(?): local i (m1 >> m2) = local i m1 >> local i m2
 
 instance (Monad m)        => RunReaderM (ReaderT    i m) i where
   local i m     = lift (runReaderT i m)
@@ -429,64 +576,75 @@
 -- | Classifies monads that support collecting the output of
 -- a sub-computation.
 class WriterM m i => RunWriterM m i | m -> i where
-  -- | Collect the output from a computation.
+  -- | Collect the output from a sub-computation.
   collect :: m a -> m (a,i)
 
+instance (Monad m,Monoid i) => RunWriterM (WriterT i m) i where
+  collect m = lift (runWriterT m)
+
 instance (RunWriterM m j) => RunWriterM (IdT m) j where
   collect (IT m) = IT (collect m)
-
 instance (RunWriterM m j) => RunWriterM (ReaderT i m) j where
   collect (R m) = R (collect . m)
-
-instance (Monad m,Monoid i) => RunWriterM (WriterT i m) i where
-  collect (W m) = lift m
-
 instance (RunWriterM m j) => RunWriterM (StateT i m) j where
   collect (S m) = S (liftM swap . collect . m)
     where swap (~(a,s),w) = ((a,w),s)
-
 instance (RunWriterM m j) => RunWriterM (ExceptionT i m) j where
   collect (X m) = X (liftM swap (collect m))
     where swap (Right a,w)  = Right (a,w)
           swap (Left x,_)   = Left x
-    -- NOTE: If the local computation fails, then the output
-    -- is discarded because the result type cannot accommodate it.
 
+-- $WriterM_ExceptionT
+--
+-- About the 'WriterM' instance:
+-- If an exception is risen while we are collecting output,
+-- then the output is lost.  If the output is important,
+-- then use 'try' to ensure that no exception may occur.
+-- Example:
+--
+-- > do (r,w) <- collect (try m)
+-- >    case r of
+-- >      Left err -> ...do something...
+-- >      Right a  -> ...do something...
 
 -- | Classifies monads that support handling of exceptions.
 class ExceptionM m i => RunExceptionM m i | m -> i where
-  -- | Exceptions are explicit in the result.
+  -- | Convert computations that may raise an exception
+  -- into computations that do not raise exception but instead,
+  -- yield a tagged results.  Exceptions are tagged with "Left",
+  -- successful computations are tagged with "Right".
   try :: m a -> m (Either i a)
 
+instance RunExceptionM IO IO.Exception where
+  try = IO.try
+
+instance (Monad m) => RunExceptionM (ExceptionT i m) i where
+  try m = lift (runExceptionT m)
+
 instance (RunExceptionM m i) => RunExceptionM (IdT m) i where
   try (IT m) = IT (try m)
-
 instance (RunExceptionM m i) => RunExceptionM (ReaderT j m) i where
   try (R m) = R (try . m)
-
 instance (RunExceptionM m i,Monoid j) => RunExceptionM (WriterT j m) i where
   try (W m) = W (liftM swap (try m))
-    where swap (Right ~(a,w)) = (Right a,w)
-          swap (Left e)       = (Left e, mempty)
-
+    where swap (Right (P a w))  = P (Right a) w
+          swap (Left e)         = P (Left e) mempty
 instance (RunExceptionM m i) => RunExceptionM (StateT j m) i where
   try (S m) = S (\s -> liftM (swap s) (try (m s)))
     where swap _ (Right ~(a,s)) = (Right a,s)
           swap s (Left e)       = (Left e, s)
 
-instance (Monad m) => RunExceptionM (ExceptionT i m) i where
-  try m = lift (runExceptionT m)
 
-
+--------------------------------------------------------------------------------
 -- Some convenient functions for working with continuations.
 
 -- | An explicit representation for continuations that store a value.
 newtype Label m a    = Lab ((a, Label m a) -> m ())
 
--- | Capture the current continuation
+-- | Capture the current continuation.
 -- This function is like 'return', except that it also captures
--- the current continuation.  Later we can use 'jump' to go back to
--- the continuation with a possibly different value.
+-- the current continuation.  Later, we can use 'jump' to repeat the
+-- computation from this point onwards but with a possibly different value.
 labelCC            :: (ContM m) => a -> m (a, Label m a)
 labelCC x           = callCC (\k -> return (x, Lab k))
 
@@ -494,71 +652,4 @@
 jump               :: (ContM m) => a -> Label m a -> m b
 jump x (Lab k)      = k (x, Lab k) >> return unreachable
   where unreachable = error "(bug) jump: unreachable"
-
-
--- | A isomorphism between (usually) monads.
--- Typically the constructor and selector of a newtype delcaration.
-data Iso m n = Iso { close :: forall a. m a -> n a,
-                     open  :: forall a. n a -> m a }
-
--- | Derive the implementation of 'fmap' from 'Functor'.
-derive_fmap :: (Functor m) => Iso m n -> (a -> b) -> n a -> n b
-derive_fmap iso f m = close iso (fmap f (open iso m))
-
--- | Derive the implementation of 'return' from 'Monad'.
-derive_return :: (Monad m) => Iso m n -> (a -> n a)
-derive_return iso a = close iso (return a)
-
--- | Derive the implementation of '>>=' from 'Monad'.
-derive_bind :: (Monad m) => Iso m n -> n a -> (a -> n b) -> n b
-derive_bind iso m k = close iso ((open iso m) >>= \x -> open iso (k x))
-
-derive_fail :: (Monad m) => Iso m n -> String -> n a
-derive_fail iso a = close iso (fail a)
-
--- | Derive the implementation of 'mfix' from 'MonadFix'.
-derive_mfix :: (MonadFix m) => Iso m n -> (a -> n a) -> n a
-derive_mfix iso f = close iso (mfix (open iso . f))
-
--- | Derive the implementation of 'ask' from 'ReaderM'.
-derive_ask :: (ReaderM m i) => Iso m n -> n i
-derive_ask iso = close iso ask
-
--- | Derive the implementation of 'put' from 'WriterM'.
-derive_put :: (WriterM m i) => Iso m n -> i -> n ()
-derive_put iso x = close iso (put x)
-
--- | Derive the implementation of 'get' from 'StateM'.
-derive_get :: (StateM m i) => Iso m n -> n i
-derive_get iso = close iso get
-
--- | Derive the implementation of 'set' from 'StateM'.
-derive_set :: (StateM m i) => Iso m n -> i -> n ()
-derive_set iso x = close iso (set x)
-
--- | Derive the implementation of 'raise' from 'ExceptionM'.
-derive_raise :: (ExceptionM m i) => Iso m n -> i -> n a
-derive_raise iso x = close iso (raise x)
-
--- | Derive the implementation of 'callCC' from 'ContM'.
-derive_callCC :: (ContM m) => Iso m n -> ((a -> n b) -> n a) -> n a
-derive_callCC iso f = close iso (callCC (open iso . f . (close iso .)))
-
--- | Derive the implementation of 'local' from 'RunReaderM'.
-derive_local :: (RunReaderM m i) => Iso m n -> i -> n a -> n a
-derive_local iso i = close iso . local i . open iso
-
--- | Derive the implementation of 'collect' from 'RunWriterM'.
-derive_collect :: (RunWriterM m i) => Iso m n -> n a -> n (a,i)
-derive_collect iso = close iso . collect . open iso
-
--- | Derive the implementation of 'try' from 'RunExceptionM'.
-derive_try :: (RunExceptionM m i) => Iso m n -> n a -> n (Either i a)
-derive_try iso = close iso . try . open iso
-
-derive_lift :: (MonadT t, Monad m) => Iso (t m) n -> m a -> n a
-derive_lift iso m = close iso (lift m)
-
-derive_inBase :: (BaseM m x) => Iso m n -> x a -> n a
-derive_inBase iso m = close iso (inBase m)
 
diff --git a/src/MonadLib/Derive.hs b/src/MonadLib/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/MonadLib/Derive.hs
@@ -0,0 +1,93 @@
+{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
+{-| This module defines a number of functions that make it easy
+to get the functionality of MonadLib for user-defined newtypes.
+-}
+module MonadLib.Derive (
+  Iso(Iso), derive_fmap, derive_return, derive_bind, derive_fail, derive_mfix,
+  derive_ask, derive_put, derive_get, derive_set, derive_raise, derive_callCC,
+  derive_local, derive_collect, derive_try,
+  derive_mzero, derive_mplus,
+  derive_lift, derive_inBase,
+) where
+
+
+import MonadLib
+import Control.Monad
+import Control.Monad.Fix
+import Prelude hiding (Ordering(..))
+
+-- | An isomorphism between (usually) monads.
+-- Typically the constructor and selector of a newtype delcaration.
+data Iso m n = Iso { close :: forall a. m a -> n a,
+                     open  :: forall a. n a -> m a }
+
+-- | Derive the implementation of 'fmap' from 'Functor'.
+derive_fmap :: (Functor m) => Iso m n -> (a -> b) -> n a -> n b
+derive_fmap iso f m = close iso (fmap f (open iso m))
+
+-- | Derive the implementation of 'return' from 'Monad'.
+derive_return :: (Monad m) => Iso m n -> (a -> n a)
+derive_return iso a = close iso (return a)
+
+-- | Derive the implementation of '>>=' from 'Monad'.
+derive_bind :: (Monad m) => Iso m n -> n a -> (a -> n b) -> n b
+derive_bind iso m k = close iso ((open iso m) >>= \x -> open iso (k x))
+
+derive_fail :: (Monad m) => Iso m n -> String -> n a
+derive_fail iso a = close iso (fail a)
+
+-- | Derive the implementation of 'mfix' from 'MonadFix'.
+derive_mfix :: (MonadFix m) => Iso m n -> (a -> n a) -> n a
+derive_mfix iso f = close iso (mfix (open iso . f))
+
+-- | Derive the implementation of 'ask' from 'ReaderM'.
+derive_ask :: (ReaderM m i) => Iso m n -> n i
+derive_ask iso = close iso ask
+
+-- | Derive the implementation of 'put' from 'WriterM'.
+derive_put :: (WriterM m i) => Iso m n -> i -> n ()
+derive_put iso x = close iso (put x)
+
+-- | Derive the implementation of 'get' from 'StateM'.
+derive_get :: (StateM m i) => Iso m n -> n i
+derive_get iso = close iso get
+
+-- | Derive the implementation of 'set' from 'StateM'.
+derive_set :: (StateM m i) => Iso m n -> i -> n ()
+derive_set iso x = close iso (set x)
+
+-- | Derive the implementation of 'raise' from 'ExceptionM'.
+derive_raise :: (ExceptionM m i) => Iso m n -> i -> n a
+derive_raise iso x = close iso (raise x)
+
+-- | Derive the implementation of 'callCC' from 'ContM'.
+derive_callCC :: (ContM m) => Iso m n -> ((a -> n b) -> n a) -> n a
+derive_callCC iso f = close iso (callCC (open iso . f . (close iso .)))
+
+-- | Derive the implementation of 'local' from 'RunReaderM'.
+derive_local :: (RunReaderM m i) => Iso m n -> i -> n a -> n a
+derive_local iso i = close iso . local i . open iso
+
+-- | Derive the implementation of 'collect' from 'RunWriterM'.
+derive_collect :: (RunWriterM m i) => Iso m n -> n a -> n (a,i)
+derive_collect iso = close iso . collect . open iso
+
+-- | Derive the implementation of 'try' from 'RunExceptionM'.
+derive_try :: (RunExceptionM m i) => Iso m n -> n a -> n (Either i a)
+derive_try iso = close iso . try . open iso
+
+-- | Derive the implementation of 'mzero' from 'MonadPlus'.
+derive_mzero :: (MonadPlus m) => Iso m n -> n a
+derive_mzero iso = close iso mzero
+
+-- | Derive the implementation of 'mplus' from 'MonadPlus'.
+derive_mplus :: (MonadPlus m) => Iso m n -> n a -> n a -> n a
+derive_mplus iso n1 n2 = close iso (mplus (open iso n1) (open iso n2))
+
+-- | Derive the implementation of 'lift' from 'MonadT'.
+derive_lift :: (MonadT t, Monad m) => Iso (t m) n -> m a -> n a
+derive_lift iso m = close iso (lift m)
+
+-- | Derive the implementation of 'inBase' from 'BaseM'.
+derive_inBase :: (BaseM m x) => Iso m n -> x a -> n a
+derive_inBase iso m = close iso (inBase m)
diff --git a/src/MonadLib/Monads.hs b/src/MonadLib/Monads.hs
new file mode 100644
--- /dev/null
+++ b/src/MonadLib/Monads.hs
@@ -0,0 +1,102 @@
+{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
+{-|  This module contains a collection of monads that
+   are defined in terms of the monad transformers from
+   "MonadLib".   The definitions in this module are
+   completely mechanical and so this module may become
+   obsolete if support for automated derivations for instances
+   becomes well supported across implementations.
+ -}
+module MonadLib.Monads (
+  Reader, Writer, State, Exception, Cont,
+  runReader, runWriter, runState, runException, runCont,
+  module MonadLib
+) where
+import MonadLib
+import MonadLib.Derive
+import Control.Monad
+import Control.Monad.Fix
+import Data.Monoid
+
+newtype Reader    i a = R' { unR :: ReaderT    i Id a }
+newtype Writer    i a = W' { unW :: WriterT    i Id a }
+newtype State     i a = S' { unS :: StateT     i Id a }
+newtype Exception i a = X' { unX :: ExceptionT i Id a }
+newtype Cont      i a = C' { unC :: ContT      i Id a }
+
+iso_R = Iso R' unR
+iso_W = Iso W' unW
+iso_S = Iso S' unS
+iso_X = Iso X' unX
+iso_C = Iso C' unC
+
+instance               BaseM (Reader    i) (Reader    i) where inBase = id
+instance (Monoid i) => BaseM (Writer    i) (Writer    i) where inBase = id
+instance               BaseM (State     i) (State     i) where inBase = id
+instance               BaseM (Exception i) (Exception i) where inBase = id
+instance               BaseM (Cont      i) (Cont      i) where inBase = id
+
+instance Monad (Reader i) where
+  return  = derive_return iso_R
+  fail    = derive_fail iso_R
+  (>>=)   = derive_bind iso_R
+
+instance (Monoid i) => Monad (Writer i) where
+  return  = derive_return iso_W
+  fail    = derive_fail iso_W
+  (>>=)   = derive_bind iso_W
+
+instance Monad (State i) where
+  return  = derive_return iso_S
+  fail    = derive_fail iso_S
+  (>>=)   = derive_bind iso_S
+
+instance Monad (Exception i) where
+  return  = derive_return iso_X
+  fail    = derive_fail iso_X
+  (>>=)   = derive_bind iso_X
+
+instance Monad (Cont i) where
+  return  = derive_return iso_C
+  fail    = derive_fail iso_C
+  (>>=)   = derive_bind iso_C
+
+instance               Functor (Reader    i) where fmap = derive_fmap iso_R
+instance (Monoid i) => Functor (Writer    i) where fmap = derive_fmap iso_W
+instance               Functor (State     i) where fmap = derive_fmap iso_S
+instance               Functor (Exception i) where fmap = derive_fmap iso_X
+instance               Functor (Cont      i) where fmap = derive_fmap iso_C
+
+instance               MonadFix (Reader    i) where mfix = derive_mfix iso_R
+instance (Monoid i) => MonadFix (Writer    i) where mfix = derive_mfix iso_W
+instance               MonadFix (State     i) where mfix = derive_mfix iso_S
+instance               MonadFix (Exception i) where mfix = derive_mfix iso_X
+
+instance ReaderM (Reader i) i where ask = derive_ask iso_R
+instance (Monoid i) => WriterM (Writer i) i where put = derive_put iso_W
+instance StateM (State i) i where get = derive_get iso_S; set = derive_set iso_S
+instance ExceptionM (Exception i) i where raise = derive_raise iso_X
+instance ContM (Cont i) where callCC = derive_callCC iso_C
+
+runReader     :: i -> Reader i a -> a
+runWriter     :: Writer i a -> (a,i)
+runState      :: i -> State i a -> (a,i)
+runException  :: Exception i a -> Either i a
+runCont       :: (a -> i) -> Cont i a -> i
+
+runReader i  = runId . runReaderT i          . unR
+runWriter    = runId . runWriterT            . unW
+runState  i  = runId . runStateT i           . unS
+runException = runId . runExceptionT         . unX
+runCont   i  = runId . runContT (return . i) . unC
+
+instance RunReaderM (Reader i) i where
+  local = derive_local iso_R
+
+instance (Monoid i) => RunWriterM (Writer i) i where
+  collect = derive_collect iso_W
+
+instance RunExceptionM (Exception i) i where
+  try = derive_try iso_X
+
+
+
diff --git a/src/Monads.hs b/src/Monads.hs
deleted file mode 100644
--- a/src/Monads.hs
+++ /dev/null
@@ -1,101 +0,0 @@
-{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
-{-|  This module contains a collection of monads that 
-   are defined in terms of the monad transformers from
-   "MonadLib".   The definitions in this module are
-   completely mechanical and so this module may become
-   obsolete if support for automated derivations for instances
-   becomes well supported across implementations.
- -}
-module Monads (
-  Reader, Writer, State, Exception, Cont, 
-  runReader, runWriter, runState, runException, runCont,
-  module MonadLib
-) where
-import MonadLib
-import Control.Monad
-import Control.Monad.Fix
-import Data.Monoid
-
-newtype Reader    i a     = R' { unR :: ReaderT     i Id a }
-newtype Writer    i a     = W' { unW :: WriterT     i Id a }
-newtype State     i a     = S' { unS :: StateT      i Id a }
-newtype Exception i a     = X' { unX :: ExceptionT  i Id a }
-newtype Cont      i a     = C' { unC :: ContT       i Id a }
-
-iso_R = Iso R' unR
-iso_W = Iso W' unW
-iso_S = Iso S' unS
-iso_X = Iso X' unX
-iso_C = Iso C' unC
-
-instance               BaseM (Reader    i) (Reader    i) where inBase = id
-instance (Monoid i) => BaseM (Writer    i) (Writer    i) where inBase = id
-instance               BaseM (State     i) (State     i) where inBase = id
-instance               BaseM (Exception i) (Exception i) where inBase = id
-instance               BaseM (Cont      i) (Cont      i) where inBase = id
-
-instance Monad (Reader i) where
-  return  = derive_return iso_R
-  fail    = derive_fail iso_R
-  (>>=)   = derive_bind iso_R
-
-instance (Monoid i) => Monad (Writer i) where
-  return  = derive_return iso_W
-  fail    = derive_fail iso_W
-  (>>=)   = derive_bind iso_W
-
-instance Monad (State i) where
-  return  = derive_return iso_S
-  fail    = derive_fail iso_S
-  (>>=)   = derive_bind iso_S
-
-instance Monad (Exception i) where
-  return  = derive_return iso_X
-  fail    = derive_fail iso_X
-  (>>=)   = derive_bind iso_X
-
-instance Monad (Cont i) where
-  return  = derive_return iso_C
-  fail    = derive_fail iso_C
-  (>>=)   = derive_bind iso_C
-
-instance               Functor (Reader    i) where fmap = derive_fmap iso_R
-instance (Monoid i) => Functor (Writer    i) where fmap = derive_fmap iso_W
-instance               Functor (State     i) where fmap = derive_fmap iso_S
-instance               Functor (Exception i) where fmap = derive_fmap iso_X
-instance               Functor (Cont      i) where fmap = derive_fmap iso_C
-
-instance               MonadFix (Reader    i) where mfix = derive_mfix iso_R
-instance (Monoid i) => MonadFix (Writer    i) where mfix = derive_mfix iso_W
-instance               MonadFix (State     i) where mfix = derive_mfix iso_S
-instance               MonadFix (Exception i) where mfix = derive_mfix iso_X
-
-instance ReaderM (Reader i) i where ask = derive_ask iso_R
-instance (Monoid i) => WriterM (Writer i) i where put = derive_put iso_W
-instance StateM (State i) i where get = derive_get iso_S; set = derive_set iso_S
-instance ExceptionM (Exception i) i where raise = derive_raise iso_X
-instance ContM (Cont i) where callCC = derive_callCC iso_C
-
-runReader     :: i -> Reader i a -> a
-runWriter     :: Writer i a -> (a,i)
-runState      :: i -> State i a -> (a,i)
-runException  :: Exception i a -> Either i a
-runCont       :: (a -> i) -> Cont i a -> i
-
-runReader i  = runId . runReaderT i          . unR
-runWriter    = runId . runWriterT            . unW
-runState  i  = runId . runStateT i           . unS
-runException = runId . runExceptionT         . unX
-runCont   i  = runId . runContT (return . i) . unC
-
-instance RunReaderM (Reader i) i where
-  local = derive_local iso_R
-
-instance (Monoid i) => RunWriterM (Writer i) i where
-  collect = derive_collect iso_W
-
-instance RunExceptionM (Exception i) i where
-  try = derive_try iso_X
-
-
-