what’s a delayed assigned mvar

Stream: lean4

[Joachim Breitner]

Today, @Kyle Miller very helpfully and patiently explained to me what delayed assigned mvars are to me, thanks for that! I thought I’d write down the explanation in my own words, in case it’s useful to anyone else.

A crucial operations on expressions is substitution (e[s/x]). But our expression have holes (metavariables) ?m, and we can’t perform the substitution until we know the value for ?m and have replaced ?m with that value. So what do we do?

We could add explicit substitution to our Expr. But that would be annoying, it’s yet another constructor to worry about at each Expr traversal, and a complex one at that (as it would likely have to be simultaneous substitution, turning Expr into a nested inductive data type). And since we can’t do much with such a unresolved substitution, just like with a normal hole ?m, we allow such substitions not everwhere, but only as the value of a MVar ?n (the “delayed assigned MVar”), and around another MVar. And because it makes things simpler, we store in ?n only x and ?m (i.e. the hole we want to substitute into and the variable in ?m’s context we want to substitute for), and keep s as an “argument” to ?n (so ?n s somewhere).

Now when instantiating MVars, when we come across the application ?n s, we can check if ?m has been assigned (to val) and then replace ?n s with val[s/x].

Maybe they should be called “MVar substituting MVars” :-)

TL;DR: If we had explicit substitution in Expr, we would not need delayed assigned mvars. In that sense, they are a mechanism that keeps such unresolved substitutions out of sight.

[Patrick Massot]

It’s nice to take time to report on this, but it will get lost very quickly. Shouldn’t you try to put that somewhere in a docstring or comment?

[Joachim Breitner]

Kyle has a PR with helpful docstrings in https://github.com/leanprover/lean4/pull/3494, so improvement will happen. I am not sure if my particular way of putting it is the most useful one, or even fully correct, anyways :-)

[Matthew Ballard]

I think you need a 4 in your repo name: you can also just lean#3494

[Kyle Miller]

That PR is an attempt to help make delayed assignment metavariables less mysterious.

If you have ever been confused why writing let f := fun x y => ?foo results in f := fun x y => ?m.123 x y, what this PR does is make it pretty print as f := fun x y => ?foo(x := x, y := y) to show that what's under the binder is ?foo with it's local variable x substituted for the binder x and it's local y for the binder y.

This linkage between ?m.123 and ?foo is called a delayed assignment. Lean maintains a table of these delayed assignments, but it does not currently expose the linkage to to the user.

[Kyle Miller]

Please give lean4#3494 a :+1: if this is a feature you think would be helpful to have. It is not currently on the roadmap, and this would be used to gauge interest.

[Kyle Miller]

The syntax ?foo(x := a, y := b) is meant to be the "Lean version" of ?foo[a/x,b/y]. Using parentheses keeps it out of the way of GetElem notation, and it also can't be confused for function application since function application must have a space after the function.

[Thomas Murrills]

To add a bit to this thread, here's what I've learned about delayed mvars (also mostly from @Kyle Miller, so thank you! :) )—it's meant to be a bit more long-form. I thought I'd put my perspective here just in case it aids understanding for anyone trying to learn about delayed mvars. :)

[Thomas Murrills]

Delayed-assigned mvars have two important (conceptual) properties that distinguish them from ordinary mvars: namely, they are what I’ll call “fvar-abstracting” and “instantiation-blocked”.

Ordinary, run-of-the-mill metavariable assignment has two important aspects. it both:

1. is constituted by data which tells us what expression a given mvar points to
2. has the effect of allowing us to instantiate that mvar to its assignment in whatever expression it appears
   These usually go hand in hand: if we assign an mvar, then we can instantiate it. Not so with delayed-assigned mvars: we have the assignment data as soon as the delayed-assigned mvar is created: we record in a table that ?m.23 points to ?a, for example. But this doesn’t have the same effect as an ordinary assignment, because we’re not allowed to instantiate the delayed-assigned mvar when it appears in expressions yet. In this sense a delayed-assigned mvar is instantiation-blocked.

This is part of why the name “delayed-assigned metavariable” is a bit confusing: the assignment itself (considered as the recording of “pointing data”) has not been delayed. (In fact, it occurs immediately, as soon as the delayed-assigned mvar is formed.) However, the effect of that assignment is delayed.

Another reason the name is a bit confusing is because it doesn’t mention the other distinctive function of delayed-assigned mvars. Delayed-assigned mvars are assigned to an mvar ?a while being aware of certain extra fvars in its context, and those fvars are themselves part of the assignment data. We might schematically write ?m.23 := ([fvars], ?a) where [fvars] is a list of (new) fvars in ?a’s local context. This kind of looks and functions like a lambda-abstraction: we might suggestively imagine this assignment as representing ?m.23 := fun fvars => ?a.

It’s in this sense that a delayed-assigned mvar like ?m.23 is fvar-abstracting: it knows what fvars to abstract in whatever it’s assigned to.

It’s important to note that an mvarId like ?a which has its fvars “abstracted” by a delayed-assigned mvar like ?m.23 knows nothing about this abstraction. All of ?a’s fvars are equivalent from ?a’s perspective. The “binding” of these fvars is known only to the delayed-assigned mvar. Hence, different delayed-assigned mvars could in principle abstract different fvars of the same mvar! This never (directly) happens in practice (unless you’re using the sneak-preview of Kyle’s fvar-substitution elaborator). But if it did, nothing would go wrong. The substitution of other terms ([xs]) for certain fvars takes place when the delayed-assigned mvar can finally be instantiated, and the ordinary mvar it’s assigned to knows nothing about this process.

There’s actually a third subtle difference between delayed-assigned mvars and ordinary ones which you’re likely implicitly aware of by now: delayed-assigned mvars are always assigned directly to ordinary mvarIds, as mvarIds are the only things that intrinsically have local contexts. It wouldn’t make sense to talk about the local context of an expression intrinsically (given how Lean works).

But why did we need to do any of this? What problems do these two properties solve? The fundamental desire is to have a metavariable ?a in fun xs => ?a whose local context effectively includes xs. Just as there are two distinctive properties of delayed-assigned mvars, there are two problems if we don’t have delayed-assigned mvars:

1. if ?a is unassigned, we don’t have a way of substituting in for the xs we want to be in its local context (suppose we were to e.g. try to beta-reduce (fun xs => ?a) [ys])
2. we have no mechanism of actually linking the bound variables xs in fun xs to the local decls in the new local context of ?a in the first place.

Instantiation-blocking solves the first problem, and fvar-abstraction solves the second.

Implementation sketch

To say that ?m.23 “behaves like a lambda expression” is equivalent to saying that for any sequence of ordinary terms [xs] which we wish to apply the lambda to, ?m.23 [xs] := ?a[fvars/xs]. To evaluate the expression ?m.23 [xs], we substitute those arguments in for the fvars in ?a which are recorded in the assignment data of ?m.23, just as we would do if the fvars were actually bound in ?m.23 and we were performing beta reduction. This is why fun xs => ?a becomes fun xs => ?m.23 xs: this is morally the same as fun xs => (fun fvars => ?a) xs, which is morally equivalent to simply fun fvars => ?a.

Lean’s implementation collapses the “abstraction” step and the “beta reduction” step into one step, and, when ?a has been fully (recursively) assigned to some expression e not containing unassigned mvars, substitutes the arguments [xs] in for the fvars occurring in e directly.

Alternate universes

But it didn’t have to be this way: instead of substituting the [xs] directly into the (fully-instantiated) expression ?a was assigned to, we could instantiate ?m.23 directly to an actual lambda ← mkLambdaFVars fvars q(?a), and then use beta-reduction on the application of this lambda to [xs]. There’s nothing wrong with this in principle—maybe performance concerns are relevant, though, I’m not sure.

Further, we don’t actually have to wait until ?a is fully-assigned to make progress during instantiation. As long as ?a is at least partially assigned (that is, assigned to something, but such that instantiating ?a may result in an expression with unassigned mvars), we could actually abstract the fvars with mkLambdaFVars during instantiation, which would “propagate the delayed assignment” by creating new delayed-assigned mvars whenever we encountered an unassigned mvar. That would abstract the appropriate fvars in those mvars. (This is how mkLambdaFvars works anyway. In fact, this is how delayed-assigned mvars get created behind the scenes when elaborating fun x => ?a!). Having created a lambda, we would then do ordinary beta reduction with [xs] instead of substituting them directly, and would be able to at least make progress instantiating a delayed-assigned mvar.

…and why we’re not in them

Another alternate way you might think of solving problem (2) (linking bound variables fun xs to the context of ?a) is with let decls: e.g. ?a gets the let decl let x := x. The reason we can’t simply do this in Lean, however, is that we’d be exposing a bound variable as a value in ?a’s context—the x on the rhs of let x := x is really #0—which would break MetaM functions. (You can’t inferType on a .bvar like #0 , for instance.) Lean would require a third kind of declaration (a .bdecl?) to even try to handle things this way, and all the complication that brings with it. Plus, this would irrevocably tie ?a to its use in that expression without careful transformations (what does #0 mean if you use ?a somewhere else?), so there are probably other contracts that this approach would break.

In a similar vein, we could use fvar-binding expression constructors: fun x => ?a could elaborate to fun x => flet x := x; ?a where flet actually did bind an fvar instead of using bound variables. This is basically equivalent to defining a substitution expression constructor, as mentioned above: flet fvars := xs; e is equivalent to e[xs/fvars] (Kyle’s elaborator essentially lets us emulate this in user-facing syntax using delayed-assigned mvars when e is a metavariable ?a as ?a(fvar := x).) But this would require two things: 1) reduction of these flets/substitutions would have to be analogously “zeta-blocked” and respect mvar (un)assignment (you couldn’t reduce flet x := x; ?a to ?a when ?a is not assigned, for example) 2) you’d now need the MetaM functions to use different local contexts at different parts of the expression to talk about well-formedness with respect to fvars. Currently, you only need a single local context at any part of the expression—for instance, a delayed-assigned mvar ?m.23 has the ambient context. Only its assignment data knows about the fvars in ?a’s local context, and that’s not part of the expression proper—it’s part of the MetaM state. But we do use telescopes to enter and manipulate binders anyway, so maybe doing the same with a let would at least be possible. Whether it would introduce more difficulties for technical reasons, though, I can’t say.

[Jannis Limperg]

If anyone would like to add an explanation along these lines to the metaprogramming book's MetaM chapter, that would be very welcome and I would be happy to review the PR. Back when I wrote that chapter, I only had a very vague understanding of delayed assignments, and the chapter reflects this.