Init.Control.State

StateT definition

(σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v)

Full source

/--
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.
-/
def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

State transformer monad

Informal description

The type `StateT σ m α` represents a monadic computation that adds a mutable state of type `σ` to the monad `m`. An action in this monad is a function that takes an initial state and returns, within the monad `m`, a pair consisting of a value of type `α` and the resulting state of type `σ`.

StateT.run definition

{σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ)

Full source

/--
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.
-/
@[always_inline, inline]
def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ) :=
  x s

Execution of state transformer (returning value and state)

Informal description

Given a state transformer monad `StateT σ m α`, an initial state `s : σ`, the function `StateT.run` executes the computation and returns, within the monad `m`, a pair consisting of the resulting value of type `α` and the final state of type `σ`.

StateT.run' definition

{σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α

Full source

/--
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.
-/
@[always_inline, inline]
def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
  (·.1) <$> x s

Execution of state transformer (discarding state)

Informal description

Given a state transformer monad `StateT σ m α`, an initial state `s : σ`, and a functor `m`, the function `StateT.run'` executes the computation and returns the resulting value of type `α` within the monad `m`, discarding the final state.

StateM definition

(σ α : Type u) : Type u

Full source

/--
A tuple-based state monad.

Actions in `StateM σ` are functions that take an initial state and return a value paired with a
final state.
-/
@[reducible]
def StateM (σ α : Type u) : Type u := StateT σ Id α

State monad

Informal description

The type `StateM σ α` represents a state monad with state type `σ` and result type `α`, implemented as a state transformer monad with the identity monad. An action in this monad is a function that takes an initial state and returns a pair consisting of a value of type `α` and the resulting state of type `σ`.

instSubsingletonStateM instance

{σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α)

Full source

instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) where
  allEq x y := by
    apply funext
    intro s
    match x s, y s with
    | (a₁, s₁), (a₂, s₂) =>
      rw [Subsingleton.elim a₁ a₂, Subsingleton.elim s₁ s₂]

Subsingleton Property of State Monad with Subsingleton State and Result Types

Informal description

For any types $\sigma$ and $\alpha$, if both $\sigma$ and $\alpha$ are subsingletons (i.e., have at most one element), then the state monad `StateM σ α` is also a subsingleton.

StateT.pure definition

(a : α) : StateT σ m α

Full source

/--
Returns the given value without modifying the state. Typically used via `Pure.pure`.
-/
@[always_inline, inline]
protected def pure (a : α) : StateT σ m α :=
  fun s => pure (a, s)

Pure operation for state transformer monad

Informal description

Given a value $a$ of type $\alpha$, the function `StateT.pure` returns a state transformer computation that, when executed with any state $s$ of type $\sigma$, produces the pair $(a, s)$ without modifying the state. This operation is typically used via `Pure.pure` to lift values into the state transformer monad.

StateT.bind definition

(x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β

Full source

/--
Sequences two actions. Typically used via the `>>=` operator.
-/
@[always_inline, inline]
protected def bind (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β :=
  fun s => do let (a, s) ← x s; f a s

Bind operation for state transformer monad

Informal description

Given a state transformer computation `x : StateT σ m α` and a function `f : α → StateT σ m β`, the operation `StateT.bind` sequences these computations by first running `x` with an initial state `s` to obtain a result `a` and a new state `s'`, then applying `f` to `a` and running the resulting computation with state `s'`.

StateT.map definition

(f : α → β) (x : StateT σ m α) : StateT σ m β

Full source

/--
Modifies the value returned by a computation. Typically used via the `<$>` operator.
-/
@[always_inline, inline]
protected def map (f : α → β) (x : StateT σ m α) : StateT σ m β :=
  fun s => do let (a, s) ← x s; pure (f a, s)

Mapping over state transformer results

Informal description

Given a function $f : \alpha \to \beta$ and a state transformer computation $x : \text{StateT} \sigma m \alpha$, the function `StateT.map` applies $f$ to the result of $x$ while preserving the state. Specifically, for an initial state $s$, it runs $x$ to obtain a pair $(a, s')$ (where $a$ is the result and $s'$ is the new state), then returns $(f(a), s')$ in the monad $m$.

StateT.instMonad instance

: Monad (StateT σ m)

Full source

@[always_inline]
instance : Monad (StateT σ m) where
  pure := StateT.pure
  bind := StateT.bind
  map  := StateT.map

Monad Instance for State Transformer

Informal description

The state transformer monad `StateT σ m` is a monad for any monad `m`, where `σ` is the type of the state. This means it supports the standard monadic operations `pure` (lifting a value into the monad) and `bind` (sequencing computations with state passing).

StateT.orElse definition

[Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m α

Full source

/--
Recovers from errors. The state is rolled back on error recovery. Typically used via the `<|>`
operator.
-/
@[always_inline, inline]
protected def orElse [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m α :=
  fun s => x₁ s <|> x₂ () s

Alternative choice for state transformers

Informal description

Given an `Alternative` monad `m`, the operation `StateT.orElse` combines two state transformer computations `x₁` and `x₂` (where `x₂` is a thunk) by attempting `x₁` first and, if it fails, falling back to `x₂`. Specifically, for an initial state `s`, it runs `x₁ s` and if that fails, it runs `x₂ () s` (applying the thunk `x₂` to the unit value and then to the state `s`).

StateT.failure definition

[Alternative m] {α : Type u} : StateT σ m α

Full source

/--
Fails with a recoverable error. The state is rolled back on error recovery.
-/
@[always_inline, inline]
protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
  fun _ => failure

Failure in state transformer monad

Informal description

The function `StateT.failure` represents a failed computation in the state transformer monad `StateT σ m`, where `m` is an `Alternative` functor. It propagates the failure behavior of the underlying monad `m` through the state transformer.

StateT.instAlternative instance

[Alternative m] : Alternative (StateT σ m)

Full source

instance [Alternative m] : Alternative (StateT σ m) where
  failure := StateT.failure
  orElse  := StateT.orElse

Alternative Instance for State Transformer Monad

Informal description

For any monad `m` that is an `Alternative` functor, the state transformer monad `StateT σ m` is also an `Alternative` functor. This means it inherits the operations `failure` and `<|>` from `m`, allowing for computations that can fail or be combined with alternative choices while maintaining state.

StateT.get definition

: StateT σ m σ

Full source

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

This increments the reference count of the state, which may inhibit in-place updates.
-/
@[always_inline, inline]
protected def get : StateT σ m σ :=
  fun s => pure (s, s)

Get current state in state transformer monad

Informal description

The function `StateT.get` retrieves the current state `s` of type `σ` in the state transformer monad `StateT σ m`, returning it as both the result and the new state (unchanged). This operation is pure and does not modify the state.

StateT.set definition

: σ → StateT σ m PUnit

Full source

/--
Replaces the mutable state with a new value.
-/
@[always_inline, inline]
protected def set : σ → StateT σ m PUnit :=
  fun s' _ => pure (⟨⟩, s')

Set state in state transformer monad

Informal description

The function `StateT.set` takes a state value `s'` of type `σ` and returns a state transformer computation that sets the current state to `s'` and returns the unit value `⟨⟩` (of type `PUnit`). This operation does not use the previous state and purely updates the state to the given value.

StateT.modifyGet definition

(f : σ → α × σ) : StateT σ m α

Full source

/--
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.
-/
@[always_inline, inline]
protected def modifyGet (f : σ → α × σ) : StateT σ m α :=
  fun s => pure (f s)

Modify and get state in state transformer monad

Informal description

The function `StateT.modifyGet` takes a function `f : σ → α × σ` and returns a state transformer computation that applies `f` to the current state `s` to produce a new value `a : α` and a new state `s' : σ`. The computation then returns `a` and sets the state to `s'`. This is equivalent to the sequence: get the current state, apply `f` to get a new value and state, set the new state, and return the new value. However, `StateT.modifyGet` may be more efficient as it avoids creating additional references to the state.

StateT.lift definition

{α : Type u} (t : m α) : StateT σ m α

Full source

/--
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](lean-manual://section/monad-lifting).
-/
@[always_inline, inline]
protected def lift {α : Type u} (t : m α) : StateT σ m α :=
  fun s => do let a ← t; pure (a, s)

Lift monadic computation into state transformer monad

Informal description

Given a monadic computation `t : m α` in the underlying monad `m`, `StateT.lift` lifts this computation into the state transformer monad `StateT σ m` without modifying the state. The resulting computation returns the value produced by `t` paired with the unchanged state. In other words, for any initial state `s : σ`, the lifted computation `StateT.lift t` executes `t` to obtain a value `a : α` and returns the pair `(a, s)`.

StateT.instMonadLift instance

: MonadLift m (StateT σ m)

Full source

instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩

Lifting Monadic Computations to State Transformer Monad

Informal description

For any monad $m$ and type $\sigma$, there is a canonical way to lift computations from $m$ to the state transformer monad $\text{StateT}\,\sigma\,m$. This lifting preserves the monadic structure while adding state handling capabilities.

StateT.instMonadFunctor instance

(σ m) : MonadFunctor m (StateT σ m)

Full source

@[always_inline]
instance (σ m) : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩

State Transformer as a Monad Functor

Informal description

For any type $\sigma$ and monad $m$, the state transformer monad $\text{StateT}\,\sigma\,m$ is a monad functor over $m$. This means there is a canonical way to lift a computation in $m$ to a computation in $\text{StateT}\,\sigma\,m$ that preserves the monadic structure while adding state handling capabilities.

StateT.instMonadExceptOf instance

(ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m)

Full source

@[always_inline]
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
  throw    := StateT.liftStateT.lift ∘ throwThe ε
  tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
}

Exception Handling in State Transformer Monads

Informal description

For any type $\sigma$, monad $m$, and exception type $\varepsilon$, if $m$ supports throwing and handling exceptions of type $\varepsilon$ (via `MonadExceptOf ε m`), then the state transformer monad $\text{StateT}\,\sigma\,m$ also supports throwing and handling exceptions of type $\varepsilon$. This means that exception handling operations (`throwThe` and `tryCatchThe`) can be lifted naturally from $m$ to $\text{StateT}\,\sigma\,m$ while preserving the state-handling behavior.

ForM.forIn definition

[Monad m] [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

Full source

/--
Creates a suitable implementation of `ForIn.forIn` from a `ForM` instance.
-/
@[always_inline, inline]
def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α]
    (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
  let g a b := .mk do
    match ← f a b with
    | .yield b' => pure (.ok (⟨⟩, b'))
    | .done b' => pure (.error b')
  match ← forM (m := StateT β (ExceptT β m)) (α := α) x g |>.run b |>.run with
  | .ok a => pure a.2
  | .error a => pure a

Monadic iteration with state and early termination

Informal description

Given a monad `m`, a container `x` of type `ρ` with elements of type `α`, an initial state `b` of type `β`, and a function `f` that processes elements of `α` with the current state `β` and returns a monadic action producing a `ForInStep β`, the function `ForM.forIn` performs a monadic iteration over the container `x`. The iteration uses a state transformer monad `StateT β (ExceptT β m)` to manage the state and early termination. The function `f` is applied to each element of `x` with the current state, and the iteration continues (`yield`) or terminates early (`done`) based on the result of `f`. The final state is returned in the monad `m`.

instMonadStateOfStateTOfMonad instance

[Monad m] : MonadStateOf σ (StateT σ m)

Full source

instance [Monad m] : MonadStateOf σ (StateT σ m) where
  get       := StateT.get
  set       := StateT.set
  modifyGet := StateT.modifyGet

State Transformer Monad as a State Monad

Informal description

For any monad `m`, the state transformer monad `StateT σ m` is a state monad with state type `σ`. This means it provides operations to get and modify the state within the monadic context.

StateT.monadControl instance

(σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m)

Full source

@[always_inline]
instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) where
  stM      := fun α   => α × σ
  liftWith := fun f => do let s ← get; liftM (f (fun x => x.run s))
  restoreM := fun x => do let (a, s) ← liftM x; setset s; pure a

Monad Control Structure for State Transformer

Informal description

For any monad $m$ and state type $\sigma$, the state transformer monad $\text{StateT}\,\sigma\,m$ has a monad control structure over $m$. This means computations in $\text{StateT}\,\sigma\,m$ can be lifted to and interpreted back in the base monad $m$, enabling automatic lifting of higher-order operations. Specifically: - There is a function that runs a computation in $\text{StateT}\,\sigma\,m$ and packages its result and state in $m$. - There is a function that reconstructs the computation in $\text{StateT}\,\sigma\,m$ from the packaged result and state in $m$.

StateT.tryFinally instance

{m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m)

Full source

@[always_inline]
instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) where
  tryFinally' := fun x h s => do
    let ((a, _), (b, s'')) ← tryFinally' (x s) fun
      | some (a, s') => h (some a) s'
      | none         => h none s
    pure ((a, b), s'')

State Transformer Monad with Finalization

Informal description

For any monad `m` with a `MonadFinally` instance and any state type `σ`, the state transformer monad `StateT σ m` also has a `MonadFinally` instance. This allows handling finalization operations (like resource cleanup) in the context of stateful computations.