instances for meta defs

Stream: metaprogramming / tactics

[Yakov Pechersky]

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?

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Reid Barton]

It already exists as a consequence of the monad instance

[Reid Barton]

Yakov Pechersky said:

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

As opposed to what?

[Yakov Pechersky]

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),

[Yakov Pechersky]

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

[Eric Wieser]

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

[Mario Carneiro]

@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

[Eric Wieser]

Oh you might have found a bug in my PR then

[Eric Wieser]

I wasn't really thinking about state rollbacks

[Eric Wieser]

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

[Mario Carneiro]

What PR?

[Eric Wieser]

lean#476

[Eric Wieser]

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?

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Gabriel Ebner]

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

[Eric Wieser]

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

[Gabriel Ebner]

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

[Reid Barton]

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

[Eric Wieser]

Ah, I see what you mean

[Eric Wieser]

Yes, that's right

[Eric Wieser]

How about release then?

[Gabriel Ebner]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

@Reid, did you see the PR?

[Reid Barton]

Yes, but I couldn't understand it

[Gabriel Ebner]

AFAIU it's a workaround for ext_simplify_core ignoring errors.

[Eric Wieser]

Exactly

[Eric Wieser]

ext_simplify_core uses errors to indicate "skip this match"

[Reid Barton]

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

[Eric Wieser]

We'd have to change the API significantly

[Reid Barton]

At the least, something like this needs way more documentation

[Eric Wieser]

Where would that documentation go?

[Reid Barton]

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

[Eric Wieser]

(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

[Eric Wieser]

find needs it too

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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.

[Reid Barton]

Because then you can write it using normal tactic functions.

[Eric Wieser]

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

[Eric Wieser]

(whatever that cleanup may be)

[Eric Wieser]

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

[Eric Wieser]

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)

[Reid Barton]

Well this all hurts my head

[Reid Barton]

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

[Reid Barton]

Can you just use mutable variables somehow?

[Reid Barton]

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

[Eric Wieser]

This isn't non-chronological

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

My claim is that nothing uses that state

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

Isn't that debug window output exactly tactic_state?

[Eric Wieser]

(I don't know the answer to this)

[Reid Barton]

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

[Reid Barton]

but what you want to do doesn't seem impossible

[Eric Wieser]

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

[Reid Barton]

ok, I give up

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

(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)