    -------------------------------------------------------------------------
    -- |
    -- Module      : Control.Monad.Logic.Class
    -- Copyright   : (c) Dan Doel
    -- License     : BSD3
    --
    -- Maintainer  : dan.doel@gmail.com
    -- Stability   : experimental
    -- Portability : non-portable (multi-parameter type classes)
    --
    -- A backtracking, logic programming monad.
    --
    --    Adapted from the paper
    --    /Backtracking, Interleaving, and Terminating
    --        Monad Transformers/, by
    --    Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry
    --    (<http://okmij.org/ftp/papers/LogicT.pdf>)
    -------------------------------------------------------------------------

    {-# LANGUAGE CPP  #-}

    #if __GLASGOW_HASKELL__ >= 702
    {-# LANGUAGE Safe #-}
    #endif

    module Control.Monad.Logic.Class (MonadLogic(..), reflect) where

    import Control.Monad.Reader
    import qualified Control.Monad.State.Lazy as LazyST
    import qualified Control.Monad.State.Strict as StrictST

    -------------------------------------------------------------------------------
    -- | Minimal implementation: msplit
    class (MonadPlus m) => MonadLogic m where
        -- | Attempts to split the computation, giving access to the first
        --   result. Satisfies the following laws:
        --
        --   > msplit mzero                == return Nothing
        --   > msplit (return a `mplus` m) == return (Just (a, m))
        msplit     :: m a -> m (Maybe (a, m a))

        -- | Fair disjunction. It is possible for a logical computation
        --   to have an infinite number of potential results, for instance:
        --
        --   > odds = return 1 `mplus` liftM (2+) odds
        --
        --   Such computations can cause problems in some circumstances. Consider:
        --
        --   > do x <- odds `mplus` return 2
        --   >    if even x then return x else mzero
        --
        --   Such a computation may never consider the 'return 2', and will
        --   therefore never terminate. By contrast, interleave ensures fair
        --   consideration of both branches of a disjunction
        interleave :: m a -> m a -> m a

        -- | Fair conjunction. Similarly to the previous function, consider
        --   the distributivity law for MonadPlus:
        --
        --   > (mplus a b) >>= k = (a >>= k) `mplus` (b >>= k)
        --
        --   If 'a >>= k' can backtrack arbitrarily many tmes, (b >>= k) may never
        --   be considered. (>>-) takes similar care to consider both branches of
        --   a disjunctive computation.
        (>>-)      :: m a -> (a -> m b) -> m b
        infixl 1 >>-

        -- | Logical conditional. The equivalent of Prolog's soft-cut. If its
        --   first argument succeeds at all, then the results will be fed into
        --   the success branch. Otherwise, the failure branch is taken.
        --   satisfies the following laws:
        --
        --   > ifte (return a) th el           == th a
        --   > ifte mzero th el                == el
        --   > ifte (return a `mplus` m) th el == th a `mplus` (m >>= th)
        ifte       :: m a -> (a -> m b) -> m b -> m b

        -- | Pruning. Selects one result out of many. Useful for when multiple
        --   results of a computation will be equivalent, or should be treated as
        --   such.
        once       :: m a -> m a

        -- | Inverts a logic computation. If @m@ succeeds with at least one value,
        -- @lnot m@ fails. If @m@ fails, then @lnot m@ succeeds the value @()@.
        lnot :: m a -> m ()

        -- All the class functions besides msplit can be derived from msplit, if
        -- desired
        interleave m1 :: m a
    m1 m2 :: m a
    m2 = m a -> m (Maybe (a, m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit m a
    m1 m (Maybe (a, m a)) -> (Maybe (a, m a) -> m a) -> m a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>=
                            m a -> ((a, m a) -> m a) -> Maybe (a, m a) -> m a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m a
    m2 (\(a :: a
    a, m1' :: m a
    m1') -> a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a m a -> m a -> m a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` m a -> m a -> m a
    forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
    interleave m a
    m2 m a
    m1')

        m :: m a
    m >>- f :: a -> m b
    f = do (a :: a
    a, m' :: m a
    m') <- m (a, m a)
    -> ((a, m a) -> m (a, m a)) -> Maybe (a, m a) -> m (a, m a)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m (a, m a)
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero (a, m a) -> m (a, m a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, m a) -> m (a, m a)) -> m (Maybe (a, m a)) -> m (a, m a)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m a -> m (Maybe (a, m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit m a
    m
                     m b -> m b -> m b
    forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
    interleave (a -> m b
    f a
    a) (m a
    m' m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
    >>- a -> m b
    f)

        ifte t :: m a
    t th :: a -> m b
    th el :: m b
    el = m a -> m (Maybe (a, m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit m a
    t m (Maybe (a, m a)) -> (Maybe (a, m a) -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= m b -> ((a, m a) -> m b) -> Maybe (a, m a) -> m b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m b
    el (\(a :: a
    a,m :: m a
    m) -> a -> m b
    th a
    a m b -> m b -> m b
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` (m a
    m m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> m b
    th))

        once m :: m a
    m = do (a :: a
    a, _) <- m (a, m a)
    -> ((a, m a) -> m (a, m a)) -> Maybe (a, m a) -> m (a, m a)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m (a, m a)
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero (a, m a) -> m (a, m a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, m a) -> m (a, m a)) -> m (Maybe (a, m a)) -> m (a, m a)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m a -> m (Maybe (a, m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit m a
    m
                    a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

        lnot m :: m a
    m = m a -> (a -> m ()) -> m () -> m ()
    forall (m :: * -> *) a b.
    MonadLogic m =>
    m a -> (a -> m b) -> m b -> m b
    ifte (m a -> m a
    forall (m :: * -> *) a. MonadLogic m => m a -> m a
    once m a
    m) (m () -> a -> m ()
    forall a b. a -> b -> a
    const m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero) (() -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    -------------------------------------------------------------------------------
    -- | The inverse of msplit. Satisfies the following law:
    --
    -- > msplit m >>= reflect == m
    reflect :: MonadLogic m => Maybe (a, m a) -> m a
    reflect :: Maybe (a, m a) -> m a
    reflect Nothing = m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
    reflect (Just (a :: a
    a, m :: m a
    m)) = a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a m a -> m a -> m a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` m a
    m

    -- An instance of MonadLogic for lists
    instance MonadLogic [] where
        msplit :: [a] -> [Maybe (a, [a])]
    msplit []     = Maybe (a, [a]) -> [Maybe (a, [a])]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, [a])
    forall a. Maybe a
    Nothing
        msplit (x :: a
    x:xs :: [a]
    xs) = Maybe (a, [a]) -> [Maybe (a, [a])]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, [a]) -> [Maybe (a, [a])])
    -> Maybe (a, [a]) -> [Maybe (a, [a])]
    forall a b. (a -> b) -> a -> b
    $ (a, [a]) -> Maybe (a, [a])
    forall a. a -> Maybe a
    Just (a
    x, [a]
    xs)

    -- | Note that splitting a transformer does
    -- not allow you to provide different input
    -- to the monadic object returned.
    -- For instance, in:
    --
    -- > let Just (_, rm') = runReaderT (msplit rm) r in runReaderT rm' r'
    --
    -- @r'@ will be ignored, because @r@ was already threaded through the
    -- computation.
    instance MonadLogic m => MonadLogic (ReaderT e m) where
        msplit :: ReaderT e m a -> ReaderT e m (Maybe (a, ReaderT e m a))
    msplit rm :: ReaderT e m a
    rm = (e -> m (Maybe (a, ReaderT e m a)))
    -> ReaderT e m (Maybe (a, ReaderT e m a))
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((e -> m (Maybe (a, ReaderT e m a)))
     -> ReaderT e m (Maybe (a, ReaderT e m a)))
    -> (e -> m (Maybe (a, ReaderT e m a)))
    -> ReaderT e m (Maybe (a, ReaderT e m a))
    forall a b. (a -> b) -> a -> b
    $ \e :: e
    e -> do Maybe (a, m a)
    r <- m a -> m (Maybe (a, m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit (m a -> m (Maybe (a, m a))) -> m a -> m (Maybe (a, m a))
    forall a b. (a -> b) -> a -> b
    $ ReaderT e m a -> e -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT e m a
    rm e
    e
                                       case Maybe (a, m a)
    r of
                                         Nothing -> Maybe (a, ReaderT e m a) -> m (Maybe (a, ReaderT e m a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, ReaderT e m a)
    forall a. Maybe a
    Nothing
                                         Just (a :: a
    a, m :: m a
    m) -> Maybe (a, ReaderT e m a) -> m (Maybe (a, ReaderT e m a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((a, ReaderT e m a) -> Maybe (a, ReaderT e m a)
    forall a. a -> Maybe a
    Just (a
    a, m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m a
    m))

    -- | See note on splitting above.
    instance MonadLogic m => MonadLogic (StrictST.StateT s m) where
        msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))
    msplit sm :: StateT s m a
    sm = (s -> m (Maybe (a, StateT s m a), s))
    -> StateT s m (Maybe (a, StateT s m a))
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT ((s -> m (Maybe (a, StateT s m a), s))
     -> StateT s m (Maybe (a, StateT s m a)))
    -> (s -> m (Maybe (a, StateT s m a), s))
    -> StateT s m (Maybe (a, StateT s m a))
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                        do Maybe ((a, s), m (a, s))
    r <- m (a, s) -> m (Maybe ((a, s), m (a, s)))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    sm s
    s)
                           case Maybe ((a, s), m (a, s))
    r of
                                Nothing          -> (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, StateT s m a)
    forall a. Maybe a
    Nothing, s
    s)
                                Just ((a :: a
    a,s' :: s
    s'), m :: m (a, s)
    m) ->
                                    (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((a, StateT s m a) -> Maybe (a, StateT s m a)
    forall a. a -> Maybe a
    Just (a
    a, (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT (\_ -> m (a, s)
    m)), s
    s')

        interleave :: StateT s m a -> StateT s m a -> StateT s m a
    interleave ma :: StateT s m a
    ma mb :: StateT s m a
    mb = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT ((s -> m (a, s)) -> StateT s m a)
    -> (s -> m (a, s)) -> StateT s m a
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                            StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    ma s
    s m (a, s) -> m (a, s) -> m (a, s)
    forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
    `interleave` StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    mb s
    s

        ma :: StateT s m a
    ma >>- :: StateT s m a -> (a -> StateT s m b) -> StateT s m b
    >>- f :: a -> StateT s m b
    f = (s -> m (b, s)) -> StateT s m b
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT ((s -> m (b, s)) -> StateT s m b)
    -> (s -> m (b, s)) -> StateT s m b
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                    StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    ma s
    s m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s)
    forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
    >>- \(a :: a
    a,s' :: s
    s') -> StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT (a -> StateT s m b
    f a
    a) s
    s'

        ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b
    ifte t :: StateT s m a
    t th :: a -> StateT s m b
    th el :: StateT s m b
    el = (s -> m (b, s)) -> StateT s m b
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT ((s -> m (b, s)) -> StateT s m b)
    -> (s -> m (b, s)) -> StateT s m b
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s -> m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s) -> m (b, s)
    forall (m :: * -> *) a b.
    MonadLogic m =>
    m a -> (a -> m b) -> m b -> m b
    ifte (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    t s
    s)
                                                    (\(a :: a
    a,s' :: s
    s') -> StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT (a -> StateT s m b
    th a
    a) s
    s')
                                                    (StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m b
    el s
    s)

        once :: StateT s m a -> StateT s m a
    once ma :: StateT s m a
    ma = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StrictST.StateT ((s -> m (a, s)) -> StateT s m a)
    -> (s -> m (a, s)) -> StateT s m a
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s -> m (a, s) -> m (a, s)
    forall (m :: * -> *) a. MonadLogic m => m a -> m a
    once (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    StrictST.runStateT StateT s m a
    ma s
    s)

    -- | See note on splitting above.
    instance MonadLogic m => MonadLogic (LazyST.StateT s m) where
        msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))
    msplit sm :: StateT s m a
    sm = (s -> m (Maybe (a, StateT s m a), s))
    -> StateT s m (Maybe (a, StateT s m a))
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT ((s -> m (Maybe (a, StateT s m a), s))
     -> StateT s m (Maybe (a, StateT s m a)))
    -> (s -> m (Maybe (a, StateT s m a), s))
    -> StateT s m (Maybe (a, StateT s m a))
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                        do Maybe ((a, s), m (a, s))
    r <- m (a, s) -> m (Maybe ((a, s), m (a, s)))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    sm s
    s)
                           case Maybe ((a, s), m (a, s))
    r of
                                Nothing -> (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, StateT s m a)
    forall a. Maybe a
    Nothing, s
    s)
                                Just ((a :: a
    a,s' :: s
    s'), m :: m (a, s)
    m) ->
                                    (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((a, StateT s m a) -> Maybe (a, StateT s m a)
    forall a. a -> Maybe a
    Just (a
    a, (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT (\_ -> m (a, s)
    m)), s
    s')

        interleave :: StateT s m a -> StateT s m a -> StateT s m a
    interleave ma :: StateT s m a
    ma mb :: StateT s m a
    mb = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT ((s -> m (a, s)) -> StateT s m a)
    -> (s -> m (a, s)) -> StateT s m a
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                            StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    ma s
    s m (a, s) -> m (a, s) -> m (a, s)
    forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
    `interleave` StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    mb s
    s

        ma :: StateT s m a
    ma >>- :: StateT s m a -> (a -> StateT s m b) -> StateT s m b
    >>- f :: a -> StateT s m b
    f = (s -> m (b, s)) -> StateT s m b
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT ((s -> m (b, s)) -> StateT s m b)
    -> (s -> m (b, s)) -> StateT s m b
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s ->
                    StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    ma s
    s m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s)
    forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
    >>- \(a :: a
    a,s' :: s
    s') -> StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT (a -> StateT s m b
    f a
    a) s
    s'

        ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b
    ifte t :: StateT s m a
    t th :: a -> StateT s m b
    th el :: StateT s m b
    el = (s -> m (b, s)) -> StateT s m b
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT ((s -> m (b, s)) -> StateT s m b)
    -> (s -> m (b, s)) -> StateT s m b
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s -> m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s) -> m (b, s)
    forall (m :: * -> *) a b.
    MonadLogic m =>
    m a -> (a -> m b) -> m b -> m b
    ifte (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    t s
    s)
                                                  (\(a :: a
    a,s' :: s
    s') -> StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT (a -> StateT s m b
    th a
    a) s
    s')
                                                  (StateT s m b -> s -> m (b, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m b
    el s
    s)

        once :: StateT s m a -> StateT s m a
    once ma :: StateT s m a
    ma = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    LazyST.StateT ((s -> m (a, s)) -> StateT s m a)
    -> (s -> m (a, s)) -> StateT s m a
    forall a b. (a -> b) -> a -> b
    $ \s :: s
    s -> m (a, s) -> m (a, s)
    forall (m :: * -> *) a. MonadLogic m => m a -> m a
    once (StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    LazyST.runStateT StateT s m a
    ma s
    s)