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)
Equations
  • StateCpsT σ m α = ((δ : Type u) → σ(ασm δ)m δ)
Instances For
    @[inline]
    def StateCpsT.runK {α : Type u} {σ : Type u} {m : Type u → Type v} {β : Type u} (x : StateCpsT σ m α) (s : σ) (k : ασm β) :
    m β
    Equations
    • x.runK s k = x β s k
    Instances For
      @[inline]
      def StateCpsT.run {α : Type u} {σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
      m (α × σ)
      Equations
      • x.run s = x.runK s fun (a : α) (s : σ) => pure (a, s)
      Instances For
        @[inline]
        def StateCpsT.run' {α : Type u} {σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
        m α
        Equations
        • x.run' s = x.runK s fun (a : α) (x : σ) => pure a
        Instances For
          @[always_inline]
          instance StateCpsT.instMonad {σ : Type u} {m : Type u → Type v} :
          Equations
          • StateCpsT.instMonad = Monad.mk
          instance StateCpsT.instLawfulMonad {σ : Type u} {m : Type u → Type v} :
          Equations
          • =
          @[always_inline]
          instance StateCpsT.instMonadStateOf {σ : Type u} {m : Type u → Type v} :
          Equations
          • One or more equations did not get rendered due to their size.
          @[inline]
          def StateCpsT.lift {α : Type u} {σ : Type u} {m : Type u → Type v} [Monad m] (x : m α) :
          StateCpsT σ m α
          Equations
          Instances For
            instance StateCpsT.instMonadLiftOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
            Equations
            • StateCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type u} => StateCpsT.lift }
            @[simp]
            theorem StateCpsT.runK_pure {α : Type u} {σ : 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} {σ : 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} {σ : 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} {σ : Type u} {m : Type u → Type v} {β : Type u} {γ : 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} {σ : Type u} {m : Type u → Type v} {β : Type u} {γ : 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} {γ : 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} {γ : 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} {γ : 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} {σ : 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} {σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
            x.run' s = x.runK s fun (a : α) (x : σ) => pure a