## Stream: general

### Topic: lifting the tactic monad

#### Scott Morrison (Aug 24 2018 at 07:50):

Several times I have wanted to use a lift of the tactic monad, in order to carry along some additional state. (As a simple example, I would like to carry along a ℕ that limits how much more computation is allowed, that several different subtactics need to respect.)

#### Scott Morrison (Aug 24 2018 at 07:52):

I've successfully written some infrastructure to do this (essentially, some typeclasses and coercions that let you move up and down from standard tactic α to stateful_tactic β α), but it was gross and hackish.

#### Scott Morrison (Aug 24 2018 at 07:52):

Is this something that others would find useful? If so, could we agree on a basic design that everyone would be happy with?

#### Johan Commelin (Aug 24 2018 at 07:53):

I think https://github.com/EdAyers/lean-humanproof/blob/a3df90b4ccd1356283e47cf56b986701944f4100/src/robot.lean#L38 might be an example of how to do that...

#### Johan Commelin (Aug 24 2018 at 07:53):

So you need to use state_t...

#### Scott Morrison (Aug 24 2018 at 07:56):

Yes --- that's exactly another example of what I have in mind.

#### Scott Morrison (Aug 24 2018 at 07:56):

The problem is now writing metatactics that are "monad polymorphic".

#### Scott Morrison (Aug 24 2018 at 07:57):

We need a typeclass that you can decorate your lift of tactic (e.g. @Edward Ayers's robot) with, that says that it really is a lift of tactic.

#### Scott Morrison (Aug 24 2018 at 08:03):

Ah, there is more in state_t than I'd seen before.

#### Scott Morrison (Aug 24 2018 at 08:32):

I think I'm still not understanding how I'm meant to use state_t. I want to be able to write something like

variables {m : Type → Type → Type} [stateful_tactic m]

meta def my_meta_tactic {α β} (f : α → β) (t : m σ α) : m σ β :=
do
get_state >>= trace, -- prints the current state, a term of type σ
r ← t,
trace r,             -- prints the result of t, a term of type α
get_state >>= trace, -- prints the new state, a term of type σ
done,
return (f r)


Here trace and done are meant to just be the standard ones from tactic, that are being automatically lifted to stateful_tactic
(such that they just preserve the σ state).

#### Scott Morrison (Aug 24 2018 at 08:45):

Clearly state_t isn't quite doing this: it doesn't even mention tactic.

#### Rob Lewis (Aug 24 2018 at 09:05):

Your m is just λ σ, state_t σ tactic. I'm not sure if the coercions from tactic are in the library, but they're very easy to write.

#### Edward Ayers (Aug 24 2018 at 10:57):

meta structure my_state :=
(my_bool : bool)
(my_nat : nat)
@[reducible] meta def state_tactic : Type → Type := state_t my_state tactic
meta def of_tactic {α} : tactic α → state_tactic α := state_t.lift
meta instance {α} : has_coe (tactic α) (state_tactic α) := ⟨of_tactic⟩
open tactic
meta def my_meta_tactic {α β : Type} (f : α → β) (t : state_tactic α) : state_tactic β :=
do
state ← get, --get the state
trace state.my_nat,
r ← t,
put {my_nat:= 100, ..state}, --set the state
done, -- done is a tactic but the coercion converts it to a state_tactic.
return $f r  #### Edward Ayers (Aug 24 2018 at 11:00): All of the alternative stuff works out of the box. <|>, guard and so on. #### Scott Morrison (Aug 24 2018 at 11:29): Thanks @Edward Ayers. This isn't quite there yet: I still want to abstract over my_state. That is, I want to be able to write my_meta_tactic so that it works with many different monads, as long as they come with a promise that they contain my_state, but possibly may carry additional state as well. #### Scott Morrison (Aug 24 2018 at 11:29): That is, sometimes I will write tactics that refer to some specific notion of state. #### Scott Morrison (Aug 24 2018 at 11:30): But other times I want to write a meta tactic that is merely sufficient polymorphic that is can pass through notions of state that other people might need. #### Edward Ayers (Aug 24 2018 at 12:02): I guess if you are only storing bools nats and strings you can use tactic.set_options as a quick fix. #### Edward Ayers (Aug 24 2018 at 12:28): I came up with a crazy idea that would solve this. The trouble is the type universes don't work and one would have to implement the dependent_dict object! --I think that you can implement this as an rbtree but it's a lot of effort. universe u constant dependent_dict (key : Type u) (α : key → Type u) : Type u namespace dependent_dict variables {key : Type u} {α : key → Type u} constant get (k : key) (d : dependent_dict key α) : option (α k) constant set (k : key) (value : α k) (d : dependent_dict key α) : dependent_dict key α end dependent_dict meta structure custom_state := (name : string) (type : Type) (default : type) -- [TODO] define an ordering according to name meta def custom_state_tactic := state_t (dependent_dict custom_state (λ c:custom_state, c.type)) tactic namespace custom_state_tactic meta def get (st : custom_state) : custom_state_tactic st.type := do d ← state_t.get, pure$ option.get_or_else (dependent_dict.get st.name d) st.default
meta def set (st : custom_state) (value : st.type) : (custom_state_tactic unit) := do
d ← state_t.get,
state_t.put (dependent_dict.set st value d)
end custom_state_tactic


#### Edward Ayers (Aug 24 2018 at 12:29):

So the idea is you would always use custom_state_tactic but define your own instance of custom_state to get the values that you care about.

#### Edward Ayers (Aug 24 2018 at 12:30):

I don't think this will work but I thought I'd share.

#### Edward Ayers (Aug 24 2018 at 12:34):

It also wouldn't work because you could give two custom_states the same name but different types, and I don't think we have decidable equality for types

#### Reid Barton (Aug 24 2018 at 15:11):

@Scott Morrison are you familiar with the design of mtl?
MonadState is your "monad that comes with a promise that it contains my_state", I think.

#### Reid Barton (Aug 24 2018 at 15:12):

But I'm not sure if this encompasses everything you want

#### Sebastian Ullrich (Aug 24 2018 at 15:33):

monad_state is already in Lean 3. A monad_tactic might be introduced in Lean 4.

#### Reid Barton (Aug 24 2018 at 15:50):

It would just be has_monad_lift_t tactic, right?

#### Reid Barton (Aug 24 2018 at 15:50):

Up to specializing names

#### Sebastian Ullrich (Aug 24 2018 at 15:56):

That is not sufficient for lifting tactic _ -> tactic _ functions or even more complex ones

#### Reid Barton (Aug 24 2018 at 16:07):

Oh, I've never actually wanted to do that with IO, and I'm not sure I trust any of the packages which claim to solve that problem anyways.

#### Reid Barton (Aug 24 2018 at 16:07):

Maybe tactic has more compelling use cases

#### Sebastian Ullrich (Aug 24 2018 at 16:12):

Yeah, it's way more important for tactic since it has a bunch of combinators like try, focus, any_goals, ...

#### Edward Ayers (Aug 28 2018 at 11:51):

Using monad_stateworks really well for me.

Last updated: May 11 2021 at 12:15 UTC