@[reducible, inline]

abbrev Control.Monad.State.State (σ α : Type) : Type

The State monad: StateT over Id.

$$\text{State}\ \sigma\ \alpha = \text{StateT}\ \sigma\ \text{Id}\ \alpha = \sigma \to (\alpha \times \sigma)$$

Equations

• Control.Monad.State.State σ α = StateT σ Id α

@[inline]

def Control.Monad.State.get {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] : StateT σ m σ

Get the current state.

$$\text{get} : \text{StateT}\ \sigma\ m\ \sigma$$

Equations

• Control.Monad.State.get = StateT.get

@[inline]

def Control.Monad.State.put {m : Type → Type u_1} {σ : Type} [Monad m] (s : σ) : StateT σ m Unit

Replace the state with a new value.

$$\text{put}(\sigma) : \text{StateT}\ \sigma\ m\ \text{Unit}$$

Equations

• Control.Monad.State.put s = StateT.set s

@[inline]

def Control.Monad.State.modify {m : Type → Type u_1} {σ : Type} [Monad m] (f : σ → σ) : StateT σ m Unit

Modify the state by applying a function.

$$\text{modify}(f) : \text{StateT}\ \sigma\ m\ \text{Unit}$$

Equations

• Control.Monad.State.modify f = StateT.modifyGet fun (s : σ) => ((), f s)

@[inline]

def Control.Monad.State.gets {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (f : σ → α) : StateT σ m α

Get a projection of the current state.

$$\text{gets}(f) = f \circ \text{get}$$

Equivalent to f <$> get.

Equations

• Control.Monad.State.gets f = do let s ← StateT.get pure (f s)

@[inline]

def Control.Monad.State.runStateT {m : Type (max u_1 u_2) → Type u_3} {σ α : Type (max u_1 u_2)} [Monad m] (ma : StateT σ m α) (s : σ) : m (α × σ)

Run a StateT computation with an initial state.

$$\text{runStateT}(ma, s_0) : m\ (\alpha \times \sigma)$$

Alias for StateT.run.

Equations

• Control.Monad.State.runStateT ma s = ma.run s

@[inline]

def Control.Monad.State.evalStateT {m : Type (max u_1 u_2) → Type u_3} {σ α : Type (max u_1 u_2)} [Functor m] [Monad m] (ma : StateT σ m α) (s : σ) : m α

Run a StateT computation, returning only the final value.

$$\text{evalStateT}(ma, s_0) : m\ \alpha$$

Equations

• Control.Monad.State.evalStateT ma s = Prod.fst <$> ma.run s

@[inline]

def Control.Monad.State.execStateT {m : Type (max u_1 u_2) → Type u_3} {σ α : Type (max u_1 u_2)} [Functor m] [Monad m] (ma : StateT σ m α) (s : σ) : m σ

Run a StateT computation, returning only the final state.

$$\text{execStateT}(ma, s_0) : m\ \sigma$$

Equations

• Control.Monad.State.execStateT ma s = Prod.snd <$> ma.run s

@[inline]

def Control.Monad.State.runState {σ α : Type} (ma : State σ α) (s : σ) : α × σ

Run a pure State computation with an initial state.

$$\text{runState}(ma, s_0) : \alpha \times \sigma$$

Equations

• Control.Monad.State.runState ma s = StateT.run ma s

@[inline]

def Control.Monad.State.evalState {σ α : Type} (ma : State σ α) (s : σ) : α

Run a pure State computation, returning only the final value.

$$\text{evalState}(ma, s_0) : \alpha$$

Equations

• Control.Monad.State.evalState ma s = (StateT.run ma s).fst

@[inline]

def Control.Monad.State.execState {σ α : Type} (ma : State σ α) (s : σ) : σ

Run a pure State computation, returning only the final state.

$$\text{execState}(ma, s_0) : \sigma$$

Equations

• Control.Monad.State.execState ma s = (StateT.run ma s).snd

theorem Control.Monad.State.runState_pure {α σ : Type} (a : α) (s : σ) : runState (pure a) s = (a, s)

runState of pure a returns (a, s). $$\text{runState}(\text{pure}\ a, s) = (a, s)$$

theorem Control.Monad.State.evalState_pure {α σ : Type} (a : α) (s : σ) : evalState (pure a) s = a

evalState of pure a returns a. $$\text{evalState}(\text{pure}\ a, s) = a$$

theorem Control.Monad.State.execState_pure {α σ : Type} (a : α) (s : σ) : execState (pure a) s = s

execState of pure a returns the initial state unchanged. $$\text{execState}(\text{pure}\ a, s) = s$$

theorem Control.Monad.State.runState_get {σ : Type} (s : σ) : runState get s = (s, s)

get returns the current state: runState get s = (s, s). $$\text{runState}(\text{get}, s) = (s, s)$$

theorem Control.Monad.State.execState_put {σ : Type} (s s' : σ) : execState (put s') s = s'

put replaces the state: execState (put s') s = s'. $$\text{execState}(\text{put}(s'), s) = s'$$