The State monad transformer using CPS style.

@[implicit_reducible]

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.2) → σ → (α → σ → m δ) → m δ)

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

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

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

@[instance_reducible, 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.

instance StateCpsT.instLawfulMonad {σ : Type u} {m : Type u → Type v} : LawfulMonad (StateCpsT σ m)

@[instance_reducible, 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.

@[instance_reducible]

instance StateCpsT.instMonadAttach {m : Type u → Type v} {ε : Type u} : MonadAttach (StateCpsT ε m)

For continuation monads, it is not possible to provide a computable MonadAttach instance that actually adds information about the return value. Therefore, this instance always attaches a proof of True.

Equations

• StateCpsT.instMonadAttach = MonadAttach.trivial

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

@[instance_reducible]

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

Equations

• StateCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.2} => StateCpsT.lift }

@[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 x ← x 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 x ← monadLift 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 a ← x (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 : PUnit → StateCpsT σ 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 : PUnit → StateCpsT σ 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