Documentation

Init.Control.State

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
    Instances For
      @[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
        Instances For
          @[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
            Instances For
              @[reducible]
              def StateM (σ α : 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
                Instances For
                  @[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
                    Instances For
                      @[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
                        Instances For
                          @[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
                            Instances For
                              @[always_inline]
                              instance StateT.instMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
                              Monad (StateT σ m)
                              Equations
                                @[inline]
                                def StateT.orElse {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
                                StateT σ m α

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

                                Equations
                                  Instances For
                                    @[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
                                      Instances For
                                        instance StateT.instAlternative {σ : Type u} {m : Type u → Type v} [Monad m] [Alternative m] :
                                        Equations
                                          @[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
                                            Instances For
                                              @[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
                                                Instances For
                                                  @[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
                                                    Instances For
                                                      @[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
                                                        Instances For
                                                          instance StateT.instMonadLift {σ : Type u} {m : Type u → Type v} [Monad m] :
                                                          MonadLift m (StateT σ m)
                                                          Equations
                                                            @[always_inline]
                                                            instance StateT.instMonadFunctor (σ : Type u_1) (m : Type u_1 → Type u_2) :
                                                            Equations
                                                              @[always_inline]
                                                              instance StateT.instMonadExceptOf {σ : Type u} {m : Type u → Type v} [Monad m] (ε : Type u_1) [MonadExceptOf ε m] :
                                                              Equations
                                                                @[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
                                                                  Instances For
                                                                    instance instMonadStateOfStateTOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
                                                                    Equations
                                                                      @[always_inline]
                                                                      instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] :
                                                                      Equations
                                                                        @[always_inline]
                                                                        instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] :
                                                                        Equations