source
def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max u v)

Adds a mutable state of type `σ` to a monad.

Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple of a value and a state.

Equations

- StateT σ m α = (σ → m (α × σ))

Instances For

source
@[inline]
def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) :
m (α × σ)

Executes an action from a monad with added state in the underlying monad `m`. Given an initial state, it returns a value paired with the final state.

Equations

- x.run s = x s

Instances For

source
@[inline]
def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :
m α

Executes an action from a monad with added state in the underlying monad `m`. Given an initial state, it returns a value, discarding the final state.

Equations

- x.run' s = (fun (x : α × σ) => x.fst) <$> x s

Instances For

source
@[reducible]
def StateM (σ α : Type u) :
Type u

A tuple-based state monad.

Actions in `StateM σ` are functions that take an initial state and return a value paired with a final state.

Equations

- StateM σ α = StateT σ Id α

Instances For

source
instance instSubsingletonStateM {σ α : Type u_1} [Subsingleton σ] [Subsingleton α] :
Subsingleton (StateM σ α)
source
@[inline]
def StateT.pure {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
StateT σ m α

Returns the given value without modifying the state. Typically used via `Pure.pure`.

Equations

- StateT.pure a s = pure (a, s)

Instances For

source
@[inline]
def StateT.bind {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) :
StateT σ m β

Sequences two actions. Typically used via the `>>=` operator.

Equations

- x.bind f s = do let __discr ← x s match __discr with | (a, s) => f a s

Instances For

source
@[inline]
def StateT.map {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) :
StateT σ m β

Modifies the value returned by a computation. Typically used via the `<$>` operator.

Equations

- StateT.map f x s = do let __discr ← x s match __discr with | (a, s) => pure (f a, s)

Instances For

source
@[always_inline]
instance StateT.instMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
Monad (StateT σ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[inline]
def StateT.orElse {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) :
StateT σ m α

Recovers from errors. The state is rolled back on error recovery. Typically used via the `<|>` operator.

Equations

- x₁.orElse x₂ s = (x₁ s <|> x₂ () s)

Instances For

source
@[inline]
def StateT.failure {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} :
StateT σ m α

Fails with a recoverable error. The state is rolled back on error recovery.

Equations

- StateT.failure x✝ = failure

Instances For

source
instance StateT.instAlternative {σ : Type u} {m : Type u → Type v} [Monad m] [Alternative m] :
Alternative (StateT σ m)
Equations

- StateT.instAlternative = { toApplicative := StateT.instMonad.toApplicative, failure := fun {α : Type ?u.23} => StateT.failure, orElse := fun {α : Type ?u.23} => StateT.orElse }

source
@[inline]
def StateT.get {σ : Type u} {m : Type u → Type v} [Monad m] :
StateT σ m σ

Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.

Equations

- StateT.get s = pure (s, s)

Instances For

source
@[inline]
def StateT.set {σ : Type u} {m : Type u → Type v} [Monad m] :
σ → StateT σ m PUnit

Replaces the mutable state with a new value.

Equations

- StateT.set s' x✝ = pure (PUnit.unit, s')

Instances For

source
@[inline]
def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σ → α × σ) :
StateT σ m α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← StateT.get); StateT.set s; pure a`. However, using `StateT.modifyGet` may lead to better performance because it doesn't add a new reference to the state value, and additional references can inhibit in-place updates of data.

Equations

- StateT.modifyGet f s = pure (f s)

Instances For

source
@[inline]
def StateT.lift {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) :
StateT σ m α

Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of automatic lifting.

Equations

- StateT.lift t s = do let a ← t pure (a, s)

Instances For

source
instance StateT.instMonadLift {σ : Type u} {m : Type u → Type v} [Monad m] :
MonadLift m (StateT σ m)
Equations

- StateT.instMonadLift = { monadLift := fun {α : Type ?u.18} => StateT.lift }

source
@[always_inline]
instance StateT.instMonadFunctor (σ : Type u_1) (m : Type u_1 → Type u_2) :
MonadFunctor m (StateT σ m)
Equations

- StateT.instMonadFunctor σ m = { monadMap := fun {α : Type ?u.19} (f : {β : Type ?u.19} → m β → m β) (x : StateT σ m α) (s : σ) => f (x s) }

source
@[always_inline]
instance StateT.instMonadExceptOf {σ : Type u} {m : Type u → Type v} [Monad m] (ε : Type u_1) [MonadExceptOf ε m] :
MonadExceptOf ε (StateT σ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[inline]
def ForM.forIn {m : Type u_1 → Type u_2} {β : Type u_1} {ρ : Type u_3} {α : Type u_4} [Monad m] [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) :
m β

Creates a suitable implementation of `ForIn.forIn` from a `ForM` instance.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance instMonadStateOfStateTOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
MonadStateOf σ (StateT σ m)
Equations

- instMonadStateOfStateTOfMonad = { get := StateT.get, set := StateT.set, modifyGet := fun {α : Type ?u.18} => StateT.modifyGet }

source
@[always_inline]
instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] :
MonadControl m (StateT σ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[always_inline]
instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] :
MonadFinally (StateT σ m)
Equations

- One or more equations did not get rendered due to their size.