Stream: Ltac2

Topic: Term syntax for variable assignments

Michael Soegtrop (Nov 11 2021 at 12:02):

@Pierre-Marie Pédrot : I have a hard time finding the term syntax for variable assignments. E.g. this doesn't work:

Ltac2 mutable x := 0.
Ltac2 Eval (Int.add 1 2).
Ltac2 Set x := 3.
Ltac2 Set x := (Int.add 1 2).

The last line fails with "Tactic definition must be a syntactical value". According to the docs this should work. Do I miss something or is this a bug?

Pierre-Marie Pédrot (Nov 11 2021 at 12:06):

Where does the doc say this is legal? Any toplevel definition, including "mutable" assignment, must be a value.

Pierre-Marie Pédrot (Nov 11 2021 at 12:06):

You need to wrap it in a thunk for this to be legal.

Pierre-Marie Pédrot (Nov 11 2021 at 12:06):

i.e. Ltac2 mutable x () := 0.

Pierre-Marie Pédrot (Nov 11 2021 at 12:07):

semantically the only reasonable way to override a definition with a non-value is from within an evaluation, but then there is https://github.com/coq/coq/pull/13982 which is stuck for some reason

Gaëtan Gilbert (Nov 11 2021 at 12:07):

having no way to evaluate and assign at top level is pretty weird for a ocaml lookalike tbh

Pierre-Marie Pédrot (Nov 11 2021 at 12:07):

I agree, but it is what it is.

Pierre-Marie Pédrot (Nov 11 2021 at 12:08):

Allowing toplevel mutability would just break everything regarding document evaluation.

Pierre-Marie Pédrot (Nov 11 2021 at 12:08):

You can't backtrack in an OCaml file...

Gaëtan Gilbert (Nov 11 2021 at 12:09):

you can in ocamldebug

Michael Soegtrop (Nov 11 2021 at 12:23):

Pierre-Marie Pédrot said:

Where does the doc say this is legal? Any toplevel definition, including "mutable" assignment, must be a value.

The error message is a bit misleading - it makes one think that it is a syntax issue and syntactically what I wrote should be allowed.

But indeed the manual says:

The body of an Ltac2 definition is required to be a syntactical value that is, a function, a constant, a pure constructor recursively applied to values or a (non-recursive) let binding of a value in a value.

The term "syntactical value" is a bit hard to grasp for me. Once evaluated a function application is also a value and it is not obvious why the Set does not evaluate its right hand side.

Pierre-Marie Pédrot (Nov 11 2021 at 12:37):

@Gaëtan Gilbert not fully, if you write to a file good luck backtracking on that

Pierre-Marie Pédrot (Nov 11 2021 at 12:39):

@Michael Soegtrop because a function can perform arbitrary effects that cannot be properly tracked at the level of the document. Imperative modification is one, but tactics can do more including local extension of the environment with constants / universes, firs-class backtrack and whatnot.

Michael Soegtrop (Nov 11 2021 at 12:43):

Well maybe we should have a concept of pure functions then.

What I am mostly after is a way to build up something like a hint database in a global variable. Hiding this in a thunk is performance wise not feasible because then at each use the database would be recreated.

I also don't see how https://github.com/coq/coq/pull/13982 increases the expressiveness of Ltac2. If the changes are local to a vernac, I could also use say some local state record with mutable fields. But I don't see a way to assign a complicated computed data structure to a global variable in Ltac2.

Pierre-Marie Pédrot (Nov 11 2021 at 12:45):

@Michael Soegtrop with that PR you can do everything as a thunk and evaluate once the value of it inside the relevant tactic, so you only have to pay once for this

Pierre-Marie Pédrot (Nov 11 2021 at 12:46):

currently this can be encoded in an impractical way by passing explicitly your hint database to the corresponding functions and evaluate the thunk at toplevel and pass that to the subcalls

Pierre-Marie Pédrot (Nov 11 2021 at 12:46):

but this is explicit, so annoying and not very modular

Pierre-Marie Pédrot (Nov 11 2021 at 12:47):

As for global tables, I agree that this should actually be provided by some dedicated primitive because it's a very common use case in tactics.

Pierre-Marie Pédrot (Nov 11 2021 at 12:47):

The catch is that one has to be careful what is stored in these tables since the same value restriction applies.

Gaëtan Gilbert (Nov 11 2021 at 12:48):

Pierre-Marie Pédrot said:

Allowing toplevel mutability would just break everything regarding document evaluation.

that's about Set, but why can't we do Ltac2 x := Int.add 1 2.?

Michael Soegtrop (Nov 11 2021 at 12:49):

Hmm I must admit I don't see the advantage of using globals here. In complicated algorithmic tactics I tend to have some sort of state record I pass around anyway. How modularity can be increased by using globals I don't see.

Pierre-Marie Pédrot (Nov 11 2021 at 12:50):

@Gaëtan Gilbert same problem, you can't store safely a potentially mutable value inside a toplevel entry. This wreaks havoc with backtrack (and serialization).

Pierre-Marie Pédrot (Nov 11 2021 at 12:50):

@Michael Soegtrop well if you already abide by the reader monad it's indeed free, but it's still annoying to have to pass this explicitly

Michael Soegtrop (Nov 11 2021 at 12:55):

Yes it is a bit annoying, but the semantics are quite obvious and a state record makes it explicit what the state is. The main downside of the PR is that IMHO the semantics are not obvious.

Michael Soegtrop (Nov 11 2021 at 13:02):

If the main issue is mutability, I would really think about having pure functional types and functions. If this is the price one has to pay for mutability, I would rather go without mutable arrays and records. Some algorithms require mutable data structures but there are usually functional alternatives which are not that much worse.

Isn't this easy to detect if a function is "pure"?

Michael Soegtrop (Nov 11 2021 at 13:04):

E.g. I would think that using search trees instead of hash tables but building them only once is more efficient than using hash tables which need to be recomputed on each use.

Pierre-Marie Pédrot (Nov 11 2021 at 13:15):

The problem is not only mutability, the effects provided by the monad (e.g. the fact we have an implicit evar map floating around) is also troublesome

Pierre-Marie Pédrot (Nov 11 2021 at 13:16):

Essentially the fact we can evaluate a Coq document in weird ways (backtrack, parallel processing, etc.) coerces us into having to be pure at the level of the metalanguage.

Pierre-Marie Pédrot (Nov 11 2021 at 13:16):

You can't just implement a hashtable in Ltac2 and hope for this to magically make sense at the level of the document.

Pierre-Marie Pédrot (Nov 11 2021 at 13:17):

The only sane place where effects can occur are in places where no vernacular command can be tampered with, i.e. in a single Ltac2 run.

Pierre-Marie Pédrot (Nov 11 2021 at 13:18):

You could have a type-and-effect system but that's very heavyweight and most of the answers will be anyways "this is impure"

Pierre-Marie Pédrot (Nov 11 2021 at 13:18):

for instance you can't even evaluate a constr in a tactic in a meaningful way

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:18):

I think you can have documents work with that, whether that's a good idea that's a different story

Pierre-Marie Pédrot (Nov 11 2021 at 13:19):

because this depends on the current environment, can generate evars / universes, etc.

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:19):

The important thing for the document is the DAG of dependencies, now it is a bit unclear

Pierre-Marie Pédrot (Nov 11 2021 at 13:19):

@Emilio Jesús Gallego Arias I can't even think of a sane semantics even with all due support from the doc manager

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:19):

but imagine we had it sorted out, so we can track what the mutable state needs, for example in terms of the univ map, etc...

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:20):

in principle you can support mutable update of a dag node

Pierre-Marie Pédrot (Nov 11 2021 at 13:20):

Ltac2 references are literally OCaml references, so you'd need to track that if you allowed them inside toplevel values

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:20):

you need to define indeed what preorder you wanna put on change propagation

Pierre-Marie Pédrot (Nov 11 2021 at 13:20):

given that you have higher order in the language it's basically hopeless

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:20):

it's easy to get a loop XD

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:21):

or lose as you mention referential transparency

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:21):

you could give referential transparency away

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:21):

but I agree maybe the sanest is not to allow it

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:21):

but as in it is possible to do, it is

Pierre-Marie Pédrot (Nov 11 2021 at 13:21):

wut? like you backtrack and replay a proof and it says something else?

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:21):

if you want to have referential transparency you need to avoid cycles on the DAG otherwise you are boom, and that's a hard problem

Pierre-Marie Pédrot (Nov 11 2021 at 13:21):

oh my

Pierre-Marie Pédrot (Nov 11 2021 at 13:22):

in any case I think this is an XY-problem

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:22):

yes, that's the whole point of the mutability

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:22):

what's the use case again?

Pierre-Marie Pédrot (Nov 11 2021 at 13:22):

defining maps of stuff at toplevel in all likeliness

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:22):

I agree with you, doesn't seem a sane idea

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:22):

Define them in a pure way, no?

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:23):

There are API such as the one in Lean that allows you to have a functional interface, but the implementation doesn't copy

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:23):

aka linearity

Pierre-Marie Pédrot (Nov 11 2021 at 13:24):

I think we need language support for toplevel maps, as a generalization of Hint databases

Pierre-Marie Pédrot (Nov 11 2021 at 13:24):

This one is sane semantically, you just keep track of the stuff in the summary / libobject as usual

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:25):

Yup, you could just allow shadowing in Ltac2

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:25):

So people can do Ltac2 my_map := empty.

Emilio Jesús Gallego Arias (Nov 11 2021 at 13:25):

and later on Ltac2 my_map := add foo my_map.

Gaëtan Gilbert (Nov 11 2021 at 13:27):

before shadowing we would need to allow my_map' := add foo my_map

Michael Soegtrop (Nov 11 2021 at 13:28):

I am not sure that a fixed top level map data structure is the solution - I am using quite different structures for different purposes.

Would it really be hopeless to have a pure subset?

Michael Soegtrop (Nov 11 2021 at 13:29):

Say only non mutable Ltac types and constr terms without evars?

Michael Soegtrop (Nov 11 2021 at 13:29):

That would be sufficient for my purposes.

Gaëtan Gilbert (Nov 11 2021 at 13:30):

Pierre-Marie Pédrot said:

for instance you can't even evaluate a constr in a tactic in a meaningful way

please explain more

Pierre-Marie Pédrot (Nov 11 2021 at 13:35):

What's the value if you backtrack (in the monad, I mean)? You can generate references that are captured by the continuation, for instance.

Pierre-Marie Pédrot (Nov 11 2021 at 13:36):

I guess you could pick the first value, but then you need to be careful to propagate the universes / evars and whatnot inside the environment.

Pierre-Marie Pédrot (Nov 11 2021 at 13:36):

This only makes sense for constrs, so in particular it means this should be a specific command, not some magic handling of terms inside the Ltac2 definition command.

Pierre-Marie Pédrot (Nov 11 2021 at 13:37):

i.e. Ltac Term foo := ....

Pierre-Marie Pédrot (Nov 11 2021 at 13:38):

(and we already have this, it's Definition foo := ltac2:(...).

Pierre-Marie Pédrot (Nov 11 2021 at 13:40):

just imagine what happens if people start storing arbitrary OCaml values in the summary, including references, functions, or worse.

Pierre-Marie Pédrot (Nov 11 2021 at 13:40):

we already had to introduce a dedicated support only for futures in the global environment...

Pierre-Marie Pédrot (Nov 11 2021 at 13:40):

(and even there it was pretty broken)

Emilio Jesús Gallego Arias (Nov 11 2021 at 14:15):

Yeah, the summary is not the right place, maybe what MIchael is facing are limitations of the proof search engine?

Emilio Jesús Gallego Arias (Nov 11 2021 at 14:15):

From a logic programming point of view, the engine is quite basic

Emilio Jesús Gallego Arias (Nov 11 2021 at 14:16):

But in my understanding, there is no free lunch here, the Coq setting is not very forgiving in that sense

Emilio Jesús Gallego Arias (Nov 11 2021 at 14:16):

using hacks such as the document are not gonna solve fundamental limitations

Last updated: Dec 07 2023 at 11:02 UTC