Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: instances for meta defs


view this post on Zulip Yakov Pechersky (Oct 08 2020 at 19:29):

Does the following make sense?

import init.meta.interactive

meta instance {state : Type} : functor (interaction_monad state) :=
{ map := λ _ _, interaction_monad_fmap,
  map_const := λ _ _ x, interaction_monad_fmap (λ _, x) }

or is that not useful, won't be accessible to the typeclass system?

view this post on Zulip Yakov Pechersky (Oct 08 2020 at 19:35):

I guess it could be something, since there is a meta instance of monad in interaction_monad.lean

view this post on Zulip Yakov Pechersky (Oct 08 2020 at 19:35):

But I don't understand why interaction_monad.result is a separate defn

view this post on Zulip Reid Barton (Oct 08 2020 at 20:12):

It already exists as a consequence of the monad instance

view this post on Zulip Reid Barton (Oct 08 2020 at 20:12):

Yakov Pechersky said:

But I don't understand why interaction_monad.result is a separate defn

As opposed to what?

view this post on Zulip Yakov Pechersky (Oct 08 2020 at 20:29):

I guess what I'm trying to understand is whether interactive_monad.result can itself be a monad or a functor. Or something similar. In lean#476, is there a way to simplify the following:

  (λ s, match found with
  | (success r s') :=  (success r s)
  | (exception f p s') := (exception f p s)
  end),

view this post on Zulip Yakov Pechersky (Oct 08 2020 at 20:29):

Which as I understand, is just replacing the state in found

view this post on Zulip Eric Wieser (Oct 08 2020 at 21:14):

I wonder if something in https://github.com/leanprover-community/lean/blob/master/library/init/control/except.lean is what I'm after

view this post on Zulip Mario Carneiro (Oct 08 2020 at 22:01):

@Yakov Pechersky There are combinators that will do most of the variations on that kind of function, but you might want to do different things with the state, e.g. rolling it back in success case but not failure

view this post on Zulip Eric Wieser (Oct 08 2020 at 22:19):

Oh you might have found a bug in my PR then

view this post on Zulip Eric Wieser (Oct 08 2020 at 22:19):

I wasn't really thinking about state rollbacks

view this post on Zulip Eric Wieser (Oct 08 2020 at 22:20):

But maybe it doesn't matter because the caller does the rollback anyway?

view this post on Zulip Mario Carneiro (Oct 08 2020 at 22:21):

What PR?

view this post on Zulip Eric Wieser (Oct 08 2020 at 22:48):

lean#476

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:21):

It looks like the operations I'm looking for are

-- capture / pack the result of a tactic
meta def capture {α : Type*} (t : tactic α) : tactic (tactic_result α) :=
λ s, match t s with
| (success r s') := success (success r s') s'
| (exception f p s') := success (exception f p s') s'
end

-- release / rethrow / unpack a captured result
meta def release {α : Type*} (t : tactic_result α) : tactic α :=
match t with
| (success r s') := return r
| e := λ s, e
end

Do these exist already under other names? If not, are the names I propose sensible?

view this post on Zulip Reid Barton (Oct 09 2020 at 14:25):

capture is similar to try_core, but returns more information. I think returning the tactic_state is generally not desirable though

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:25):

The sole purpose of capture is to put the result through release later

view this post on Zulip Reid Barton (Oct 09 2020 at 14:25):

In particular I'm skeptical about the | e := λ s, e case

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:27):

Which is equivalent to | (exception f p s') := λ s, (exception f p s'), right? Presumably you're worried the second s' should be s?

view this post on Zulip Gabriel Ebner (Oct 09 2020 at 14:27):

capture t is just t <$> read, right?

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:28):

Doesn't docs#read give me a tactic (tactic_state), not tactic (tactic_result α)?

view this post on Zulip Gabriel Ebner (Oct 09 2020 at 14:28):

And a tactic is a function from tactic_state to tactic_result α.

view this post on Zulip Reid Barton (Oct 09 2020 at 14:28):

oh, I was looking for read but I thought it would be called get

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:29):

Ah, I see what you mean

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:29):

Yes, that's right

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:29):

How about release then?

view this post on Zulip Gabriel Ebner (Oct 09 2020 at 14:29):

release r is almost λ _, r, except that it doesn't update the tactic state.

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:30):

It leaves it unupdated for exceptions, but updates it for success

view this post on Zulip Reid Barton (Oct 09 2020 at 14:30):

Really I'm just skeptical about this entire endeavor I guess. Manipulating these tactic_states directly is like a worse version of GOTO.

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:30):

@Reid, did you see the PR?

view this post on Zulip Reid Barton (Oct 09 2020 at 14:31):

Yes, but I couldn't understand it

view this post on Zulip Gabriel Ebner (Oct 09 2020 at 14:31):

AFAIU it's a workaround for ext_simplify_core ignoring errors.

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:31):

Exactly

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:31):

ext_simplify_core uses errors to indicate "skip this match"

view this post on Zulip Reid Barton (Oct 09 2020 at 14:31):

Do we have to work around it? Could we fix it instead?

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:31):

We'd have to change the API significantly

view this post on Zulip Reid Barton (Oct 09 2020 at 14:31):

At the least, something like this needs way more documentation

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:32):

Where would that documentation go?

view this post on Zulip Reid Barton (Oct 09 2020 at 14:33):

In probably like an 80-line block comment above the definition of conv.interactive.for

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:33):

(note that I'm modelling the name capture from https://outcome.readthedocs.io/en/latest/api.html#outcome.capture). I suppose to match that, I should use unwrap instead of release

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:33):

find needs it too

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:35):

This is why I'm suggesting the two defs above - they leave a nice place for some explanatory documentation of why they can be useful

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:35):

Even if one of them is just t <$> read

view this post on Zulip Reid Barton (Oct 09 2020 at 14:37):

Eric Wieser said:

Which is equivalent to | (exception f p s') := λ s, (exception f p s'), right? Presumably you're worried the second s' should be s?

I'm definitely less worried if the second s' is s.

view this post on Zulip Reid Barton (Oct 09 2020 at 14:37):

Because then you can write it using normal tactic functions.

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:38):

That would give an incorrect error message though. I want to see the tactic state at the point the error happened, not at the point that ext_simplify_core did its cleanup after that

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:38):

(whatever that cleanup may be)

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:38):

I don't believe the tactic state in exception is used for anything other than diagnostics

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:38):

Trying to continue from an error state by extracting and using the s of exception would be foolish in any situation - if you recover from an error, you should resume from a known-good state (ie, the beginning of a try)

view this post on Zulip Reid Barton (Oct 09 2020 at 14:42):

Well this all hurts my head

view this post on Zulip Reid Barton (Oct 09 2020 at 14:42):

I think maybe only 80 lines will not be enough? :upside_down:

view this post on Zulip Reid Barton (Oct 09 2020 at 14:42):

Can you just use mutable variables somehow?

view this post on Zulip Reid Barton (Oct 09 2020 at 14:45):

I really think that whatever you are trying to do should be possible without this weird non-chronological control flow

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:45):

This isn't non-chronological

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:46):

This is just a rewind, which is exactly what try {} already does - the only difference is I'm rewinding to an error state, not to the pre-error state

view this post on Zulip Reid Barton (Oct 09 2020 at 14:46):

Isn't it? You're saving an intermediate state and using it later, after more things might have affected the state in the meantime

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:46):

My claim is that nothing uses that state

view this post on Zulip Reid Barton (Oct 09 2020 at 14:46):

Yeah but try doesn't give you an object to use in totally uncontrolled ways

view this post on Zulip Reid Barton (Oct 09 2020 at 14:47):

So then you must not need it, right? :upside_down:

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:47):

Sorry, my claim is that the only user of the third argument to exception is the debug window printout

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:47):

And for that use case, the old state is the one that matters

view this post on Zulip Reid Barton (Oct 09 2020 at 14:48):

And you can't just capture the debug window output locally in a thunk or something?

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:48):

Isn't that debug window output exactly tactic_state?

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:48):

(I don't know the answer to this)

view this post on Zulip Reid Barton (Oct 09 2020 at 14:49):

Like, if the tactic monad was the IO monad, your implementation would be impossible

view this post on Zulip Reid Barton (Oct 09 2020 at 14:49):

but what you want to do doesn't seem impossible

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:49):

What I want to do would be impossible in the IO monad

view this post on Zulip Reid Barton (Oct 09 2020 at 14:49):

ok, I give up

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:50):

If I have a print_with_commas some_monad that ignores errors in some_monad and keeps printing commas, there's nothing I can do to stop those commas being printed

view this post on Zulip Eric Wieser (Oct 09 2020 at 14:50):

But in the tactic monad, I can (and need to) rollback time to before the commas are printed. try {} is also not possible in the IO monad

view this post on Zulip Eric Wieser (Oct 09 2020 at 15:10):

Thanks for the feedback, anyway - I'll see if I can make the intent clearer

view this post on Zulip Reid Barton (Oct 09 2020 at 15:24):

I still think it would be better to fix the API of ext_simplify_core so that it doesn't swallow all exceptions--this might fix other bugs at the same time.

view this post on Zulip Eric Wieser (Oct 09 2020 at 15:25):

My main resistance to that is ext_simplify_core being written in C++

view this post on Zulip Eric Wieser (Oct 09 2020 at 15:26):

But yes, I suppose the signature of the pre and postcallbacks to ext_simplify_core could be changed from returning tactic (α × expr × option expr × bool) to returning tactic $ option (α × expr × option expr × bool), where none in the new version means monadic failure means together

view this post on Zulip Eric Wieser (Oct 09 2020 at 15:29):

But that requires changing every single caller of ext_simplify_core, which is something I don't feel at all comfortable doing.

view this post on Zulip Eric Wieser (Oct 09 2020 at 16:07):

I've updated the PR code with some more comments, and the PR description to summarize the alternative I describe above.

view this post on Zulip Mario Carneiro (Oct 10 2020 at 01:09):

Eric Wieser said:

But that requires changing every single caller of ext_simplify_core, which is something I don't feel at all comfortable doing.

There aren't that many, because it's a very unwieldy API

view this post on Zulip Eric Wieser (Oct 10 2020 at 07:12):

There are a fair number of transitive callers that would change too

view this post on Zulip Eric Wieser (Oct 10 2020 at 07:16):

Would a suitable compromise be to:

  • Define a wrapper, ext_simplify_core_strict, which does the monad tricks currently in the PR
  • Change find and for to use this def instead
  • Slowly convert other callers to use the new API over multiple PRs
  • Change the C++ API to make ext_simplify_core_strict the default behavior, once all callers are changed

I don't want to have to perform a massive refactor to fix an annoying bug - I'd prefer to fix the bug first, and leave breadcrumbs for someone more competent to perform the refactor

view this post on Zulip Eric Wieser (Oct 13 2020 at 10:18):

(note that this was merged in the end, and @Gabriel Ebner pointed out that ext_simplify_core not only discards errors, but rolls back any changes to the tactic state)


Last updated: May 09 2021 at 23:10 UTC