Normalisation by evaluation

[ollef]

Andras Kovacs has written a nice overview of why normalisation by evaluation (NbE) is a good idea for performance over at the Dhall Discourse.

I'm very fond of having well-typed variable bindings, as we have when using the bound library, and not e.g. De Brujin indices/levels as integers, but maybe we can figure out a way to achieve that with NbE as well?

If we later implement "gluing" as well, as in smalltt, it seems like we can get mad performance! The important point there seems to be to not let meta variable solutions grow arbitrarily big.

Another education implementation is here: https://github.com/jozefg/nbe-for-mltt/

[brendanzab]

I've been using this too in rust-nbe-for-mltt (precipitated by pikelet-lang/pikelet#181 and based on nbe-for-mltt), it's very nice!

[ollef]

There are some experiments happening over at https://github.com/ollef/sixty.

Cheers @brendanzab! I'll probably bug you for help when I get stuck.

[brendanzab]

Sure thing - are you planning on using levels + indices at the moment? Or sticking with names?

Currently trying to port over Andras' algorithm for metavariable solving (sans gluing): pikelet-lang/pikelet#8 (comment)

I'm also currently stuck with porting the fat bar in Wadler's pattern matching compilation algorithm. Hopefully will make more progress soon.

Yes, please bug me as needed!

[ollef]

It depends on how the experiment goes. I'm a bit worried that the "no substitution" trick will break down when you get to pattern matching elaboration, because you then need to make replacements in the middle of environments. This requires shifts both with indices and levels. Do you have any ideas there?

Sixten is not using names, by the way, but the Bound library for bound variables (so basically De Bruijn indices) and globally unique identifiers (represented by numbers) for free variables. Unique identifiers don't ever need shifting when elaborating patterns, but you also can't go under binders without substitution.

Cool! I'll be attempting metavars soon as well.

Just shout if you wanna discuss fat bars.

[brendanzab]

I'm a bit worried that the "no substitution" trick will break down when you get to pattern matching elaboration, because you then need to make replacements in the middle of environments.

Yeah, I'm wondering if we can think up any tricks to work with that.

In my pattern compilation I do the following:

• add definitions to the elaboration context for each scrutinee, remebering the level of each one
• manually add name-level substitutions to the elaboration context as I hit binders
• when I'm finished, I add let bindings for each scrutinee

[ollef]

Your approach seems to solve the index shifting problem, but don't the values still have levels that need to be shifted (in the other direction) as well?

I wonder if instead of levels it might be worthwhile to use globally unique identifiers for values, like in Sixten. It would require a bit more work than plain arithmetic to convert from value identifier to syntax index, e.g. a context lookup (or something more clever?), but that might be okay.

[brendanzab]

but don't the values still have levels that need to be shifted (in the other direction) as well?

Isn't that not an issue because your elaboration target should always be the syntax? Levels are only even produced from elaboration.

[ollef]

I could be wrong, but I think it's still an issue: If we're adding bindings in the middle of the context, the values that are already in the context will have levels that refer to indices as the context was before adding the bindings, and readback will then give us the wrong result.

Levels give us free weakening provided we only add to the end of the context, but with dependent pattern matching elaboration, we're making changes potentially anywhere in the context depending on the index of the variable we're matching on.

You can set things up so that you're never removing anything from the context though, which I've done in Sixten. This means that globally unique variables can still work without substitution.

[brendanzab]

When do you need to add the values to the middle of the context? I'm still kind of confused about that. Is there a way you can rearrange it so that you introduce the values before you need them?

Might be interesting to see if @AndrasKovacs has any thoughts re. pattern matching compilation.

[ollef]

When elaborating case x of Con y z -> rhs, you replace x in the context with y, z. Or, like I do in Sixten to avoid removing entries, put y, z just before x in the context, and set x = Con y z.

I would also love to hear what Andras has to say on this. :)

[AndrasKovacs]

I only have some experience with elaborating minitt/cubicaltt style case splits, which behave like LambdaCase from Haskell. Those are pretty simple to elaborate because there is no case scrutinee.

[brendanzab]

When elaborating case x of Con y z -> rhs, you replace x in the context with y, z. Or, like I do in Sixten to avoid removing entries, put y, z just before x in the context, and set x = Con y z.

I would also love to hear what Andras has to say on this. :)

Ah yeah, I think I have a way around that - by adding the scrutinees to the context, remembering the level where they were defined, and adding them as let bindings at the end. But it's a little icky and I've not sorted through all the things I need to do for that.

[ollef]

Hmm, I think I need your solution spelled out to understand it.

What we need for dependent matching is that when typechecking rhs in case x of Con y z -> rhs, any occurrences of x in the context are convertible to Con y z. Do you get that?

[ollef]

I've solved this problem in Sixty, which now has pattern matching elaboration, by decoupling the De Bruijn indices from the context indices, keeping a mapping from the former to the latter during type checking. I believe this approach would work both when using levels and unique identifiers in the domain.

[brendanzab]

Oh nice! Do you have a link to where this is done in Sixty?

[ollef]

Sure, check out the Context module.

In the context, there's indices which maintains the De Bruijn index to Var mapping (where Var is the type of domain variables), and boundVars, which maintains the order of the variables in context and has a slightly misleading name.

This allows us to both extend the context at the right end, which is done in the extend function, and extend the context somewhere in the middle, which is done in extendBefore. Notice that extendBefore still extends the indices to the right.

[brendanzab]

Cool, thanks! So you've switched back to levels + indices in Sixty from names + HOAS?

[ollef]

It's names in the presyntrax, indices in the syntax, and unique identifiers in the domain. It might be possible to back to levels in the domain, actually, if I'm not forgetting something.