mathlib documentation

• run : σ → m (α × σ)

• 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.

• 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