Zulip Chat Archive

Stream: lean4

Topic: universe polymorphic lambdas in metaprogramming

Thomas Murrills (May 17 2023 at 06:53):

Let's say I morally want to create a lambda of the form

fun {u} {α : Type u} => <body>

at the meta level. This is of course impossible as written—but what's the best way to emulate this in metaprogramming?

If I use a universe mvar, then applying this lambda expr as an argument to functions like mkAppM' yields an application type mismatch error—I'm not sure how to tell lean to unify the mvar appropriately. The unification doesn't happen automatically.

Or, maybe I could use some kind of intermediate, behind-the-scenes addDecl to get a universe polymorphic constant with actual params, then use that in lieu of a lambda.

I'm still kind of hazy on the difference between level params and level mvars, except that params are...sort of like binding names for universes? And a constant having certain level params u, v, ... in its ConstantInfo effectively binds these names in its type? Maybe? I really don't know. (Pointers to reading material/module docs are welcome! I couldn't find one in the file Level was defined.)

Which of these approaches is viable (if either)—or is there a better approach?

Mario Carneiro (May 17 2023 at 06:54):

level params are like fvar, level mvars are like mvar

Mario Carneiro (May 17 2023 at 06:54):

you want a level bvar and those don't exist

Mario Carneiro (May 17 2023 at 06:55):

you could just keep a level fvar and remember the fvar name along with it

Mario Carneiro (May 17 2023 at 06:56):

This is also basically what ConstantInfo does: it uses fvars for the universe variables, but it holds a list of fvar names so that they can be substituted later

Mario Carneiro (May 17 2023 at 06:57):

a ConstantInfo is morally a fun {u1 ... un} => <actual value> after all

Thomas Murrills (May 17 2023 at 07:03):

Hmmm, okay...! So I could make a fresh level param and turn it into a level, say u, construct the lambda e.g. fun {α : Type u} (a : α) => <body>—but then to apply this to some argument a' at the meta level...I guess I'd have to 1) look at the type of the type of the actual argument a' and get its level, then 2) replace u in the lambda with that level (then mkAppM' would hopefully work). Is that the cleanest way of doing this?

Thomas Murrills (May 17 2023 at 07:04):

It kind of feels like universe mvars would be useful here, but I'm not sure how to make unification happen. (Or if universe mvars really behave like expr mvars...)

Mario Carneiro (May 17 2023 at 07:19):

mvars would also work, although you can only assign them once, if you want to instantiate this thing multiple times you will need different mvars for each case

Mario Carneiro (May 17 2023 at 07:19):

and they need to be in the mvar context, so they aren't suitable for long term storage like ConstantInfo

Thomas Murrills (May 17 2023 at 07:20):

oh, that's great to know! (I do indeed need to apply it to things more than once)

Thomas Murrills (May 17 2023 at 07:21):

but that does make the function that returns this lambda a bit awkward, since I suppose it's also got to return these new level params.

Thomas Murrills (May 17 2023 at 07:22):

and maybe...add them to some state to prevent the same one from being generated again later on and clashing?

Thomas Murrills (May 17 2023 at 07:22):

do I need to worry about that?

Mario Carneiro (May 17 2023 at 07:23):

no, the name generator has the context to ensure the name is not reused

Mario Carneiro (May 17 2023 at 07:23):

which you will get as long as you are in a monad extending CoreM

Thomas Murrills (May 17 2023 at 07:23):

ok, great. this is in forallBoundedTelescope I maybe should mention. Not sure if that resets the whole state or just the cache

Mario Carneiro (May 17 2023 at 07:24):

the name generator is never reset

Thomas Murrills (May 17 2023 at 07:24):

that's a relief!

Thomas Murrills (May 17 2023 at 07:24):

is that because it's special-cased, or is it one of a bunch of things that's never reset?

Mario Carneiro (May 17 2023 at 07:25):

the latter

Mario Carneiro (May 17 2023 at 07:25):

the default situation is for things not to be reset, unless they are in the "backtrackable state" from MonadBacktrack

Mario Carneiro (May 17 2023 at 07:27):

oh I lied, the entire Core.State is in the backtrackable state

Mario Carneiro (May 17 2023 at 07:27):

including ngen

Thomas Murrills (May 17 2023 at 07:29):

aah, okay, gotcha, good to know! (I knew about the backtrackable state but did assume that almost everything was in it)

Thomas Murrills (May 17 2023 at 07:30):

though I looked at forallBoundedTelescope and it looks like the *Telescopes don't actually backtrack the state anyway, maybe?

Mario Carneiro (May 17 2023 at 07:31):

no, unless you use <|> or saveState and s.restore or similar it won't backtrack

Thomas Murrills (May 17 2023 at 07:32):

cool, yeah, I'm pretty sure it just modifies the things it says it modifies via withReader (and that's it)

Mario Carneiro (May 17 2023 at 07:32):

why would it?

Mario Carneiro (May 17 2023 at 07:32):

I don't think it even ever fails

Thomas Murrills (May 17 2023 at 07:33):

It at least restores "the cache" after executing its argument, and I wasn't sure how far that went

Mario Carneiro (May 17 2023 at 07:34):

I don't think it restores anything

Mario Carneiro (May 17 2023 at 07:34):

it runs the continuation in an extended context, that's it

Mario Carneiro (May 17 2023 at 07:34):

it's in the reader context so there is nothing to restore

Thomas Murrills (May 17 2023 at 07:34):

Given type of the form forall xs, A, execute k xs A.This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

Thomas Murrills (May 17 2023 at 07:35):

Right, I know that now that I've looked at the code :)

Thomas Murrills (May 17 2023 at 07:35):

But I wasn't sure just from the docstring.

Mario Carneiro (May 17 2023 at 07:38):

Mario Carneiro said:

oh I lied, the entire Core.State is in the backtrackable state

Oh I lied again, although the backtrackable state stores the whole Core.State, s.restore only pulls some fields out and leaves the rest, and the ngen is not restored

Thomas Murrills (May 17 2023 at 07:41):

aha! interesting. I wonder why everything that's not backtracked is in the backtrackable state, then...

Mario Carneiro (May 17 2023 at 07:45):

probably to avoid copying lots of things if saveState is called more often than restore

Thomas Murrills (May 17 2023 at 07:52):

Huh, ok—same kind of deal as how referring to just part of an array (and also the whole thing) causes it to get copied?

Thomas Murrills (May 17 2023 at 07:53):

Anyway! Cool. Manual management of level params! I've got to turn in but ty for the info, this was very illuminating. :)

Mario Carneiro (May 17 2023 at 08:56):

Thomas Murrills said:

Huh, ok—same kind of deal as how referring to just part of an array (and also the whole thing) causes it to get copied?

No, these data structures are shared either way. It's more that you have to copy less pointers around

Last updated: Dec 20 2023 at 11:08 UTC