0 | module Control.Monad.State.State
  1 |
  2 | import Control.Monad.Identity
  3 | import Control.Monad.Trans
  4 |
  5 | %default total
  6 |
  7 | ||| A monad transformer extending an inner monad `m` with state `stateType`.
  8 | |||
  9 | ||| Updates to the state are applied in the order as the sequence of actions.
 10 | public export
 11 | record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
 12 |   constructor ST
 13 |   runStateT' : stateType -> m (stateType, a)
 14 |
 15 | ||| Unwrap and apply a StateT monad computation.
 16 | public export
 17 | %inline
 18 | runStateT : stateType -> StateT stateType m a -> m (stateType, a)
 19 | runStateT s act = runStateT' act s
 20 |
 21 | ||| Unwrap and apply a StateT monad computation, but discard the final state.
 22 | public export %inline
 23 | evalStateT : Functor m => stateType -> StateT stateType m a -> m a
 24 | evalStateT s = map snd . runStateT s
 25 |
 26 | ||| Unwrap and apply a StateT monad computation, but discard the resulting value.
 27 | public export %inline
 28 | execStateT : Functor m => stateType -> StateT stateType m a -> m stateType
 29 | execStateT s = map fst . runStateT s
 30 |
 31 | ||| Map both the return value and final state of a computation using
 32 | ||| the given function.
 33 | public export %inline
 34 | mapStateT : (m (s, a) -> n (s, b)) -> StateT s m a -> StateT s n b
 35 | mapStateT f m = ST $ f . runStateT' m
 36 |
 37 | --------------------------------------------------------------------------------
 38 | --          State
 39 | --------------------------------------------------------------------------------
 40 |
 41 | ||| The State monad. See the MonadState interface
 42 | public export
 43 | State : (stateType : Type) -> (ty : Type) -> Type
 44 | State = \s, a => StateT s Identity a
 45 |
 46 | ||| Unwrap and apply a State monad computation.
 47 | public export %inline
 48 | runState : stateType -> State stateType a -> (stateType, a)
 49 | runState s act = runIdentity (runStateT s act)
 50 |
 51 | ||| Unwrap and apply a State monad computation, but discard the final state.
 52 | public export %inline
 53 | evalState : stateType -> State stateType a -> a
 54 | evalState s = snd . runState s
 55 |
 56 | ||| Unwrap and apply a State monad computation, but discard the resulting value.
 57 | public export %inline
 58 | execState : stateType -> State stateType a -> stateType
 59 | execState s = fst . runState s
 60 |
 61 | ||| Map both the return value and final state of a computation using
 62 | ||| the given function.
 63 | public export %inline
 64 | mapState : ((s, a) -> (s, b)) -> State s a -> State s b
 65 | mapState f = mapStateT $ \(Id p) => Id (f p)
 66 |
 67 | --------------------------------------------------------------------------------
 68 | --          Implementations
 69 | --------------------------------------------------------------------------------
 70 |
 71 | public export
 72 | implementation Functor f => Functor (StateT stateType f) where
 73 |     map f (ST g) = ST $ \st => map f <$> g st
 74 |
 75 | public export
 76 | implementation Monad f => Applicative (StateT stateType f) where
 77 |     pure x = ST $ \st => pure (st, x)
 78 |
 79 |     ST f <*> ST a
 80 |         = ST $ \st =>
 81 |                do (r, g) <- f st
 82 |                   (t, b) <- a r
 83 |                   pure (t, g b)
 84 |
 85 | public export
 86 | implementation Monad m => Monad (StateT stateType m) where
 87 |     ST f >>= k
 88 |         = ST $ \st =>
 89 |                do (st', v) <- f st
 90 |                   runStateT st' $ k v
 91 |
 92 | public export
 93 | implementation MonadTrans (StateT stateType) where
 94 |     lift x = ST $ \st => (st,) <$> x
 95 |
 96 | public export
 97 | implementation (Monad f, Alternative f) => Alternative (StateT st f) where
 98 |     empty = lift empty
 99 |     ST f <|> mg = ST $ \st => f st <|> runStateT' mg st
100 |
101 | public export
102 | implementation HasIO m => HasIO (StateT stateType m) where
103 |   liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)
104 |