Zulip Chat Archive

Stream: general

Topic: lifting the tactic monad


view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Aug 24 2018 at 07:53):

So you need to use state_t...

view this post on Zulip Scott Morrison (Aug 24 2018 at 07:56):

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

view this post on Zulip Scott Morrison (Aug 24 2018 at 07:56):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 24 2018 at 08:03):

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

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Aug 24 2018 at 08:45):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Edward Ayers (Aug 24 2018 at 11:00):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 24 2018 at 11:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Aug 24 2018 at 12:30):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 24 2018 at 15:12):

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

view this post on Zulip Sebastian Ullrich (Aug 24 2018 at 15:33):

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

view this post on Zulip Reid Barton (Aug 24 2018 at 15:50):

It would just be has_monad_lift_t tactic, right?

view this post on Zulip Reid Barton (Aug 24 2018 at 15:50):

Up to specializing names

view this post on Zulip Sebastian Ullrich (Aug 24 2018 at 15:56):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 24 2018 at 16:07):

Maybe tactic has more compelling use cases

view this post on Zulip 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, ...

view this post on Zulip Edward Ayers (Aug 28 2018 at 11:51):

Using monad_stateworks really well for me.


Last updated: May 11 2021 at 12:15 UTC