The State monad transformer using CPS style.

source
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

- StateCpsT σ m α = ((δ : Type ?u.21) → σ → (α → σ → m δ) → m δ)

Instances For

source
@[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

- x.runK s k = x β s k

Instances For

source
@[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

- x.run s = x.runK s fun (a : α) (s : σ) => pure (a, s)

Instances For

source
@[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

- x.run' s = x.runK s fun (a : α) (x : σ) => pure a

Instances For

source
@[always_inline]
instance StateCpsT.instMonad {σ : Type u} {m : Type u → Type v} :
Monad (StateCpsT σ m)
Equations

- One or more equations did not get rendered due to their size.

source
instance StateCpsT.instLawfulMonad {σ : Type u} {m : Type u → Type v} :
LawfulMonad (StateCpsT σ m)
source
@[always_inline]
instance StateCpsT.instMonadStateOf {σ : Type u} {m : Type u → Type v} :
MonadStateOf σ (StateCpsT σ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[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

- StateCpsT.lift x x✝ s k = do let x ← x k x s

Instances For

source
instance StateCpsT.instMonadLiftOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
MonadLift m (StateCpsT σ m)
Equations

- StateCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.18} => StateCpsT.lift }

source
@[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
source
@[simp]
theorem StateCpsT.runK_get {σ : Type u} {m : Type u → Type v} {β : Type u} (s : σ) (k : σ → σ → m β) :
get.runK s k = k s s
source
@[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'
source
@[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)
source
@[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 x ← x k x s
source
@[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 x ← monadLift x k x s
source
@[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
source
@[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 a ← x (f a).runK s k
source
@[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
source
@[simp]
theorem StateCpsT.runK_bind_set {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) :
(set s' >>= f).runK s k = (f PUnit.unit).runK s' k
source
@[simp]
theorem StateCpsT.runK_bind_modify {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) :
(modify f >>= g).runK s k = (g PUnit.unit).runK (f s) k
source
@[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)
source
@[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