Documentation

Init.Control.StateCps

The State monad transformer using CPS style.

def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max (u + 1) v)

An alternative implementation of a state monad transformer that internally uses continuation passing style instead of tuples.

Equations
    Instances For
      @[inline]
      def StateCpsT.runK {α σ : Type u} {m : Type u → Type v} {β : Type u} (x : StateCpsT σ m α) (s : σ) (k : ασm β) :
      m β

      Runs a stateful computation that's represented using continuation passing style by providing it with an initial state and a continuation.

      Equations
        Instances For
          @[inline]
          def StateCpsT.run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ 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.

          While the state is internally represented in continuation passing style, the resulting value is the same as for a non-CPS state monad.

          Equations
            Instances For
              @[inline]
              def StateCpsT.run' {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ 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
                  @[always_inline]
                  instance StateCpsT.instMonad {σ : Type u} {m : Type u → Type v} :
                  Equations
                    instance StateCpsT.instLawfulMonad {σ : Type u} {m : Type u → Type v} :
                    @[always_inline]
                    instance StateCpsT.instMonadStateOf {σ : Type u} {m : Type u → Type v} :
                    Equations
                      @[inline]
                      def StateCpsT.lift {α σ : Type u} {m : Type u → Type v} [Monad m] (x : m α) :
                      StateCpsT σ 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 StateCpsT.instMonadLiftOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
                          Equations
                            @[simp]
                            theorem StateCpsT.runK_pure {α σ : Type u} {m : Type u → Type v} {β : Type u} (a : α) (s : σ) (k : ασm β) :
                            (pure a).runK s k = k a s
                            @[simp]
                            theorem StateCpsT.runK_get {σ : Type u} {m : Type u → Type v} {β : Type u} (s : σ) (k : σσm β) :
                            get.runK s k = k s s
                            @[simp]
                            theorem StateCpsT.runK_set {σ : Type u} {m : Type u → Type v} {β : Type u} (s s' : σ) (k : PUnitσm β) :
                            (set s').runK s k = k PUnit.unit s'
                            @[simp]
                            theorem StateCpsT.runK_modify {σ : Type u} {m : Type u → Type v} {β : Type u} (f : σσ) (s : σ) (k : PUnitσm β) :
                            (modify f).runK s k = k PUnit.unit (f s)
                            @[simp]
                            theorem StateCpsT.runK_lift {α σ : Type u} {m : Type u → Type v} {β : Type u} [Monad m] (x : m α) (s : σ) (k : ασm β) :
                            (StateCpsT.lift x).runK s k = do let xx k x s
                            @[simp]
                            theorem StateCpsT.runK_monadLift {α σ : Type u} {m : Type u → Type v} {n : Type u → Type u_1} {β : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : ασm β) :
                            (monadLift x).runK s k = do let xmonadLift x k x s
                            @[simp]
                            theorem StateCpsT.runK_bind_pure {α σ : Type u} {m : Type u → Type v} {β γ : Type u} (a : α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
                            (pure a >>= f).runK s k = (f a).runK s k
                            @[simp]
                            theorem StateCpsT.runK_bind_lift {α σ : Type u} {m : Type u → Type v} {β γ : Type u} [Monad m] (x : m α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
                            (StateCpsT.lift x >>= f).runK s k = do let ax (f a).runK s k
                            @[simp]
                            theorem StateCpsT.runK_bind_get {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σStateCpsT σ m β) (s : σ) (k : βσm γ) :
                            (get >>= f).runK s k = (f s).runK s k
                            @[simp]
                            theorem StateCpsT.runK_bind_set {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : PUnitStateCpsT σ m β) (s s' : σ) (k : βσm γ) :
                            (set s' >>= f).runK s k = (f PUnit.unit).runK s' k
                            @[simp]
                            theorem StateCpsT.runK_bind_modify {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σσ) (g : PUnitStateCpsT σ m β) (s : σ) (k : βσm γ) :
                            (modify f >>= g).runK s k = (g PUnit.unit).runK (f s) k
                            @[simp]
                            theorem StateCpsT.run_eq {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
                            x.run s = x.runK s fun (a : α) (s : σ) => pure (a, s)
                            @[simp]
                            theorem StateCpsT.run'_eq {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
                            x.run' s = x.runK s fun (a : α) (x : σ) => pure a