mathlib documentation

core / init.control.state

structure state_t (σ : Type u) (m : Type uType v) (α : Type u) :
Type (max u v)
  • run : σ → m × σ)
def state (σ α : Type u) :
Type u
Equations
@[protected]
def state_t.pure {σ : Type u} {m : Type uType v} [monad m] {α : Type u} (a : α) :
state_t σ m α
Equations
@[protected]
def state_t.bind {σ : Type u} {m : Type uType v} [monad m] {α β : Type u} (x : state_t σ m α) (f : α → state_t σ m β) :
state_t σ m β
Equations
  • x.bind f = λ (s : σ), x.run s >>= λ (_p : α × σ), state_t.bind._match_1 f _p
  • state_t.bind._match_1 f (a, s') = (f a).run s'
@[protected, instance]
def state_t.monad {σ : Type u} {m : Type uType v} [monad m] :
monad (state_t σ m)
Equations
@[protected]
def state_t.orelse {σ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) :
state_t σ m α
Equations
@[protected]
def state_t.failure {σ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} :
state_t σ m α
Equations
@[protected, instance]
def state_t.alternative {σ : Type u} {m : Type uType v} [monad m] [alternative m] :
Equations
@[protected]
def state_t.get {σ : Type u} {m : Type uType v} [monad m] :
state_t σ m σ
Equations
@[protected]
def state_t.put {σ : Type u} {m : Type uType v} [monad m] :
σ → state_t σ m punit
Equations
@[protected]
def state_t.modify {σ : Type u} {m : Type uType v} [monad m] (f : σ → σ) :
Equations
@[protected]
def state_t.lift {σ : Type u} {m : Type uType v} [monad m] {α : Type u} (t : m α) :
state_t σ m α
Equations
@[protected, instance]
def state_t.has_monad_lift {σ : Type u} {m : Type uType v} [monad m] :
Equations
@[protected]
def state_t.monad_map {σ : Type u_1} {m : Type u_1Type u_2} {m' : Type u_1Type u_3} [monad m] [monad m'] {α : Type u_1} (f : Π {α : Type u_1}, m αm' α) :
state_t σ m αstate_t σ m' α
Equations
@[protected, instance]
def state_t.monad_functor (σ : Type u_1) (m m' : Type u_1Type u_2) [monad m] [monad m'] :
monad_functor m m' (state_t σ m) (state_t σ m')
Equations
@[protected]
def state_t.adapt {σ σ' σ'' α : Type u} {m : Type uType v} [monad m] (split : σ → σ' × σ'') (join : σ' → σ'' → σ) (x : state_t σ' m α) :
state_t σ m α
Equations
  • state_t.adapt split join x = λ (st : σ), state_t.adapt._match_2 join x (split st)
  • state_t.adapt._match_2 join x (st, ctx) = x.run st >>= λ (_p : α × σ'), state_t.adapt._match_1 join ctx _p
  • state_t.adapt._match_1 join ctx (a, st') = pure (a, join st' ctx)
@[protected, instance]
def state_t.monad_except {σ : Type u} {m : Type uType v} [monad m] (ε : out_param (Type u_1)) [monad_except ε m] :
Equations
@[class]
structure monad_state (σ : out_param (Type u)) (m : Type uType v) :
Type (max (u+1) v)
  • lift : Π {α : Type ?}, state σ αm α

An implementation of MonadState. In contrast to the Haskell implementation, we use overlapping instances to derive instances automatically from monad_lift.

Note: This class can be seen as a simplification of the more "principled" definition

class monad_state_lift (σ : out_param (Type u)) (n : Type u  Type u) :=
(lift {α : Type u} : ( {m : Type u  Type u} [monad m], state_t σ m α)  n α)

which better describes the intent of "we can lift a state_t from anywhere in the monad stack". However, by parametricity the types ∀ m [monad m], σ → m (α × σ) and σ → α × σ should be equivalent because the only way to obtain an m is through pure.

Instances
@[protected, instance]
def monad_state_trans {σ : Type u} {m : Type uType v} {n : Type uType w} [monad_state σ m] [has_monad_lift m n] :
Equations
@[protected, instance]
def state_t.monad_state {σ : Type u} {m : Type uType v} [monad m] :
Equations
def get {σ : Type u} {m : Type uType v} [monad m] [monad_state σ m] :
m σ

Obtain the top-most state of a monad stack.

Equations
def put {σ : Type u} {m : Type uType v} [monad m] [monad_state σ m] (st : σ) :

Set the top-most state of a monad stack.

Equations
def modify {σ : Type u} {m : Type uType v} [monad m] [monad_state σ m] (f : σ → σ) :

Map the top-most state of a monad stack.

Note: modify f may be preferable to f <$> get >>= put because the latter does not use the state linearly (without sufficient inlining).

Equations
@[class]
structure monad_state_adapter (σ σ' : out_param (Type u)) (m m' : Type uType v) :
Type (max (u+1) v)
  • adapt_state : Π {σ'' α : Type ?}, (σ' → σ × σ'')(σ → σ'' → σ')m αm' α

Adapt a monad stack, changing the type of its top-most state.

This class is comparable to Control.Lens.Zoom, but does not use lenses (yet?), and is derived automatically for any transformer implementing monad_functor.

For zooming into a part of the state, the split function should split σ into the part σ' and the "context" σ'' so that the potentially modified σ' and the context can be rejoined by join in the end. In the simplest case, the context can be chosen as the full outer state (ie. σ'' = σ), which makes split and join simpler to define. However, note that the state will not be used linearly in this case.

Example:

def zoom_fst {α σ σ' : Type} : state σ α  state (σ × σ') α :=
adapt_state id prod.mk

The function can also zoom out into a "larger" state, where the new parts are supplied by split and discarded by join in the end. The state is therefore not used linearly anymore but merely affinely, which is not a practically relevant distinction in Lean.

Example:

def with_snd {α σ σ' : Type} (snd : σ') : state (σ × σ') α  state σ α :=
adapt_state (λ st, ((st, snd), ())) (λ st,snd _, st)

Note: This class can be seen as a simplification of the more "principled" definition

class monad_state_functor (σ σ' : out_param (Type u)) (n n' : Type u  Type u) :=
(map {α : Type u} : ( {m : Type u  Type u} [monad m], state_t σ m α  state_t σ' m α)  n α  n' α)

which better describes the intent of "we can map a state_t anywhere in the monad stack". If we look at the unfolded type of the first argument ∀ m [monad m], (σ → m (α × σ)) → σ' → m (α × σ'), we see that it has the lens type ∀ f [functor f], (α → f α) → β → f β with f specialized to λ σ, m (α × σ) (exercise: show that this is a lawful functor). We can build all lenses we are insterested in from the functions split and join as

λ f _ st, let (st, ctx) := split st in
          (λ st', join st' ctx) <$> f st
Instances
@[protected, instance]
def monad_state_adapter_trans {σ σ' : Type u} {m m' n n' : Type uType v} [monad_state_adapter σ σ' m m'] [monad_functor m m' n n'] :
Equations
@[protected, instance]
def state_t.monad_state_adapter {σ σ' : Type u} {m : Type uType v} [monad m] :
monad_state_adapter σ σ' (state_t σ m) (state_t σ' m)
Equations
@[protected, instance]
def state_t.monad_run (σ : Type u_1) (m : Type u_1Type u_2) (out : out_param (Type u_1Type u_2)) [monad_run out m] :
monad_run (λ (α : Type u_1), σ → out × σ)) (state_t σ m)
Equations