lifting the tactic monad

Stream: general

[Scott Morrison]

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]

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]

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]

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]

So you need to use state_t...

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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

[Rob Lewis]

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]

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]

All of the alternative stuff works out of the box. <|>, guard and so on.

[Scott Morrison]

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]

That is, sometimes I will write tactics that refer to some specific notion of state.

[Scott Morrison]

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]

I guess if you are only storing bools nats and strings you can use tactic.set_options as a quick fix.

[Edward Ayers]

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]

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]

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

[Edward Ayers]

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]

@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]

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

[Sebastian Ullrich]

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

[Reid Barton]

It would just be has_monad_lift_t tactic, right?

[Reid Barton]

Up to specializing names

[Sebastian Ullrich]

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

[Reid Barton]

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]

Maybe tactic has more compelling use cases

[Sebastian Ullrich]

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

[Edward Ayers]

Using monad_stateworks really well for me.