Safe Haskell	None
Language	Haskell2010

Agda.Utils.StrictState

Description

This is a plain strict state monad, where state update, monadic binding and return are all strict. If you only need a single strict state effect, use this module.

Do not use Control.Monad.State.Strict for the same purpose; it's not even strict in state updates and is much less amenable to GHC optimizations than this module.

Synopsis

class Monad m => MonadState s (m :: Type -> Type) | m -> s where
- get :: m s
- put :: s -> m ()
- state :: (s -> (a, s)) -> m a
evalState :: State s a -> s -> a
evalStateT :: Monad m => StateT s m a -> s -> m a
execState :: State s a -> s -> s
execStateT :: Monad m => StateT s m a -> s -> m s
gets :: MonadState s m => (s -> a) -> m a
modify :: MonadState s m => (s -> s) -> m ()
runState :: State s a -> s -> (a, s)
runStateT :: Monad m => StateT s m a -> s -> m (a, s)
newtype State s a = State {
- runState# :: s -> (# a, s #)
}
newtype StateT s (m :: Type -> Type) a = StateT {
- runStateT# :: s -> m (Pair a s)
}

Documentation

class Monad m => MonadState s (m :: Type -> Type) | m -> s where #

Minimal definition is either both of get and put or just state

Minimal complete definition

state | get, put

Methods

get :: m s #

Return the state from the internals of the monad.

put :: s -> m () #

Replace the state inside the monad.

state :: (s -> (a, s)) -> m a #

Embed a simple state action into the monad.

Instances

Instances details

MonadState NiceState Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceState # put :: NiceState -> Nice () # state :: (NiceState -> (a, NiceState)) -> Nice a #
MonadState ParseState LexAction Source #
Instance details Defined in Agda.Syntax.Parser.Alex Methods get :: LexAction ParseState # put :: ParseState -> LexAction () # state :: (ParseState -> (a, ParseState)) -> LexAction a #
MonadState ParseState Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState # put :: ParseState -> Parser () # state :: (ParseState -> (a, ParseState)) -> Parser a #
MonadState NLMState NLM Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods get :: NLM NLMState # put :: NLMState -> NLM () # state :: (NLMState -> (a, NLMState)) -> NLM a #
Monad m => MonadState FreshThings (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods get :: PureConversionT m FreshThings # put :: FreshThings -> PureConversionT m () # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a #
MonadState s m => MonadState s (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods get :: NamesT m s # put :: s -> NamesT m () # state :: (s -> (a, s)) -> NamesT m a #
MonadState s m => MonadState s (ListT m) Source #
Instance details Defined in Agda.Utils.ListT Methods get :: ListT m s # put :: s -> ListT m () # state :: (s -> (a, s)) -> ListT m a #
MonadState s (State s) Source #
Instance details Defined in Agda.Utils.StrictState Methods get :: State s s # put :: s -> State s () # state :: (s -> (a, s)) -> State s a #
MonadState s m => MonadState s (CatchT m) #
Instance details Defined in Control.Monad.Catch.Pure Methods get :: CatchT m s # put :: s -> CatchT m () # state :: (s -> (a, s)) -> CatchT m a #
MonadState s m => MonadState s (MaybeT m) #
Instance details Defined in Control.Monad.State.Class Methods get :: MaybeT m s # put :: s -> MaybeT m () # state :: (s -> (a, s)) -> MaybeT m a #
MonadState s m => MonadState s (ReaderT r m) Source #
Instance details Defined in Agda.Utils.StrictReader Methods get :: ReaderT r m s # put :: s -> ReaderT r m () # state :: (s -> (a, s)) -> ReaderT r m a #
Monad m => MonadState s (StateT s m) Source #
Instance details Defined in Agda.Utils.StrictState Methods get :: StateT s m s # put :: s -> StateT s m () # state :: (s -> (a, s)) -> StateT s m a #
(Monoid w, MonadState s m) => MonadState s (AccumT w m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.State.Class Methods get :: AccumT w m s # put :: s -> AccumT w m () # state :: (s -> (a, s)) -> AccumT w m a #
MonadState s m => MonadState s (ExceptT e m) #	Since: mtl-2.2
Instance details Defined in Control.Monad.State.Class Methods get :: ExceptT e m s # put :: s -> ExceptT e m () # state :: (s -> (a, s)) -> ExceptT e m a #
MonadState s m => MonadState s (IdentityT m) #
Instance details Defined in Control.Monad.State.Class Methods get :: IdentityT m s # put :: s -> IdentityT m () # state :: (s -> (a, s)) -> IdentityT m a #
MonadState s m => MonadState s (ReaderT r m) #
Instance details Defined in Control.Monad.State.Class Methods get :: ReaderT r m s # put :: s -> ReaderT r m () # state :: (s -> (a, s)) -> ReaderT r m a #
MonadState s m => MonadState s (SelectT r m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.State.Class Methods get :: SelectT r m s # put :: s -> SelectT r m () # state :: (s -> (a, s)) -> SelectT r m a #
Monad m => MonadState s (StateT s m) #
Instance details Defined in Control.Monad.State.Class Methods get :: StateT s m s # put :: s -> StateT s m () # state :: (s -> (a, s)) -> StateT s m a #
Monad m => MonadState s (StateT s m) #
Instance details Defined in Control.Monad.State.Class Methods get :: StateT s m s # put :: s -> StateT s m () # state :: (s -> (a, s)) -> StateT s m a #
(Monoid w, MonadState s m) => MonadState s (WriterT w m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.State.Class Methods get :: WriterT w m s # put :: s -> WriterT w m () # state :: (s -> (a, s)) -> WriterT w m a #
(Monoid w, MonadState s m) => MonadState s (WriterT w m) #
Instance details Defined in Control.Monad.State.Class Methods get :: WriterT w m s # put :: s -> WriterT w m () # state :: (s -> (a, s)) -> WriterT w m a #
(Monoid w, MonadState s m) => MonadState s (WriterT w m) #
Instance details Defined in Control.Monad.State.Class Methods get :: WriterT w m s # put :: s -> WriterT w m () # state :: (s -> (a, s)) -> WriterT w m a #
MonadState s m => MonadState s (ContT r m) #
Instance details Defined in Control.Monad.State.Class Methods get :: ContT r m s # put :: s -> ContT r m () # state :: (s -> (a, s)) -> ContT r m a #
(Monad m, Monoid w) => MonadState s (RWST r w s m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.State.Class Methods get :: RWST r w s m s # put :: s -> RWST r w s m () # state :: (s -> (a, s)) -> RWST r w s m a #
(Monad m, Monoid w) => MonadState s (RWST r w s m) #
Instance details Defined in Control.Monad.State.Class Methods get :: RWST r w s m s # put :: s -> RWST r w s m () # state :: (s -> (a, s)) -> RWST r w s m a #
(Monad m, Monoid w) => MonadState s (RWST r w s m) #
Instance details Defined in Control.Monad.State.Class Methods get :: RWST r w s m s # put :: s -> RWST r w s m () # state :: (s -> (a, s)) -> RWST r w s m a #
MonadState st m => MonadState st (EquivT s c v m) #
Instance details Defined in Data.Equivalence.Monad Methods get :: EquivT s c v m st # put :: st -> EquivT s c v m () # state :: (st -> (a, st)) -> EquivT s c v m a #
MonadState [ParseWarning] PM Source #
Instance details Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] # put :: [ParseWarning] -> PM () # state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a #

evalState :: State s a -> s -> a Source #

evalStateT :: Monad m => StateT s m a -> s -> m a Source #

execState :: State s a -> s -> s Source #

execStateT :: Monad m => StateT s m a -> s -> m s Source #

gets :: MonadState s m => (s -> a) -> m a Source #

modify :: MonadState s m => (s -> s) -> m () Source #

runState :: State s a -> s -> (a, s) Source #

runStateT :: Monad m => StateT s m a -> s -> m (a, s) Source #

newtype State s a Source #

Constructors

State
Fields runState# :: s -> (# a, s #)

Instances

Instances details

MonadState s (State s) Source #
Instance details Defined in Agda.Utils.StrictState Methods get :: State s s # put :: s -> State s () # state :: (s -> (a, s)) -> State s a #
Applicative (State s) Source #
Instance details Defined in Agda.Utils.StrictState Methods pure :: a -> State s a # (<>) :: State s (a -> b) -> State s a -> State s b # liftA2 :: (a -> b -> c) -> State s a -> State s b -> State s c # (>) :: State s a -> State s b -> State s b # (<*) :: State s a -> State s b -> State s a #
Functor (State s) Source #
Instance details Defined in Agda.Utils.StrictState Methods fmap :: (a -> b) -> State s a -> State s b # (<$) :: a -> State s b -> State s a #
Monad (State s) Source #
Instance details Defined in Agda.Utils.StrictState Methods (>>=) :: State s a -> (a -> State s b) -> State s b # (>>) :: State s a -> State s b -> State s b # return :: a -> State s a #