- run : σ → m (α × σ)
Instances for state_t
- state_t.has_sizeof_inst
- state_t.monad
- state_t.alternative
- state_t.has_monad_lift
- state_t.monad_functor
- state_t.monad_except
- state_t.monad_state
- state_t.monad_state_adapter
- state_t.monad_run
- state_t.is_lawful_monad
- linarith.linarith_monad.monad
- linarith.linarith_monad.monad_except
- state_t.monad_writer
- state_t.monad_cont
- state_t.is_lawful_monad_cont
- state_t.uliftable
- rand_g.uliftable
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
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 of this typeclass
Instances of other typeclasses for monad_state
- monad_state.has_sizeof_inst
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:
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 of this typeclass
Instances of other typeclasses for monad_state_adapter
- monad_state_adapter.has_sizeof_inst
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}