Documentation

Init.Control.StateRef

def StateRefT' (ω σ : Type) (m : TypeType) (α : Type) :

A state monad that uses an actual mutable reference cell (i.e. an ST.Ref ω σ).

The macro StateRefT σ m α infers ω from m. It should normally be used instead.

Equations
    Instances For

      Recall that StateRefT is a macro that infers ω from the m.

      @[inline]
      def StateRefT'.run {ω σ : Type} {m : TypeType} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ 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.

      The monad m must support ST effects in order to create and mutate reference cells.

      Equations
        Instances For
          @[inline]
          def StateRefT'.run' {ω σ : Type} {m : TypeType} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ 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.

          The monad m must support ST effects in order to create and mutate reference cells.

          Equations
            Instances For
              @[inline]
              def StateRefT'.lift {ω σ : Type} {m : TypeType} {α : Type} (x : m α) :
              StateRefT' ω σ 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 StateRefT'.instMonad {ω σ : Type} {m : TypeType} [Monad m] :
                  Monad (StateRefT' ω σ m)
                  Equations
                    instance StateRefT'.instMonadLift {ω σ : Type} {m : TypeType} :
                    MonadLift m (StateRefT' ω σ m)
                    Equations
                      instance StateRefT'.instMonadFunctor {ω : Type} (σ : Type) (m : TypeType) :
                      Equations
                        instance StateRefT'.instAlternativeOfMonad {ω σ : Type} {m : TypeType} [Alternative m] [Monad m] :
                        Equations
                          @[inline]
                          def StateRefT'.get {ω σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] :
                          StateRefT' ω σ 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 StateRefT'.set {ω σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] (s : σ) :

                              Replaces the mutable state with a new value.

                              Equations
                                Instances For
                                  @[inline]
                                  def StateRefT'.modifyGet {ω σ : Type} {m : TypeType} {α : Type} [MonadLiftT (ST ω) m] (f : σα × σ) :
                                  StateRefT' ω σ 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 a get followed by a set. However, using modifyGet may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

                                  Equations
                                    Instances For
                                      instance StateRefT'.instMonadStateOfOfMonadLiftTST {ω σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] :
                                      Equations
                                        @[always_inline]
                                        instance StateRefT'.instMonadExceptOf {ω σ : Type} {m : TypeType} (ε : Type u_1) [MonadExceptOf ε m] :
                                        Equations
                                          instance instMonadControlStateRefT' (ω σ : Type) (m : TypeType) :
                                          Equations
                                            instance instMonadFinallyStateRefT' {m : TypeType} {ω σ : Type} [MonadFinally m] :
                                            Equations