Equations
- state_t.pure a = ⟨λ (s : σ), has_pure.pure (a, s)⟩
Equations
Equations
- state_t.failure = ⟨λ (s : σ), failure⟩
Equations
- state_t.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u) (x : _x → _x_1) (y : state_t σ m _x), has_pure.pure x <*> y, map_const := λ (α β : Type u), (λ (x : β → α) (y : state_t σ m β), has_pure.pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type u) (a : state_t σ m α) (b : state_t σ m β), (λ (_x _x_1 : Type u) (x : _x → _x_1) (y : state_t σ m _x), has_pure.pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u) (a : state_t σ m α) (b : state_t σ m β), (λ (_x _x_1 : Type u) (x : _x → _x_1) (y : state_t σ m _x), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := state_t.orelse _inst_2}, failure := state_t.failure _inst_2}
Equations
- state_t.get = ⟨λ (s : σ), has_pure.pure (s, s)⟩
Equations
- state_t.put = λ (s' : σ), ⟨λ (s : σ), has_pure.pure (punit.star, s')⟩
Equations
- state_t.modify f = ⟨λ (s : σ), has_pure.pure (punit.star, f s)⟩
Equations
- state_t.lift t = ⟨λ (s : σ), t >>= λ (a : α), has_pure.pure (a, s)⟩
Equations
- state_t.has_monad_lift = {monad_lift := state_t.lift _inst_1}
Equations
- state_t.monad_functor σ m m' = {monad_map := state_t.monad_map _inst_3}
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') = has_pure.pure (a, join st' ctx)
Equations
- state_t.monad_except ε = {throw := λ (α : Type u), state_t.lift ∘ monad_except.throw, catch := λ (α : Type u) (x : state_t σ m α) (c : ε → state_t σ m α), ⟨λ (s : σ), monad_except.catch (x.run s) (λ (e : ε), (c e).run s)⟩}
- 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
lean
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.
Equations
- monad_state_trans = {lift := λ (α : Type u) (x : state σ α), has_monad_lift_t.monad_lift (monad_state.lift x)}
Equations
- state_t.monad_state = {lift := λ (α : Type u) (x : state σ α), ⟨λ (s : σ), has_pure.pure (x.run s)⟩}
Obtain the top-most state of a monad stack.
Equations
Set the top-most state of a monad stack.
Equations
- put st = monad_state.lift (state_t.put st)
- 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:
lean
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:
lean
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
lean
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
lean
λ f _ st, let (st, ctx) := split st in
(λ st', join st' ctx) <$> f st
Equations
- monad_state_adapter_trans = {adapt_state := λ (σ'' α : Type u) (split : σ' → σ × σ'') (join : σ → σ'' → σ'), monad_functor_t.monad_map (λ (α : Type u), monad_state_adapter.adapt_state split join)}
Equations
- state_t.monad_state_adapter = {adapt_state := λ (σ'' α : Type u), state_t.adapt}
Equations
- state_t.monad_run σ m out = {run := λ (α : Type u_1) (x : state_t σ m α), monad_run.run ∘ λ (σ_1 : σ), x.run σ_1}