Conversation

The basics are the same. Notable difference: evaluation/conversion should be non-type directed, types shouldn't appear in semantics; it's both simpler and faster. Andreas Abel & Danny use types to eta expand nfs and check conversion on nfs...

Instead we should check conversion on semantic values directly, and it's known that eta for Pi and Sigma are decidable in purely syntax-directed way. The result is that types don't appear in evaluation, nor do we have to build up useless intermediate nfs just to check conversion

I could give detailed answers in other places, I'm not sure where, maybe on github.

(syntax-directed eta doesn't work for unit type, but in that case it's better to handle eta in the elaborator, by tagging irrelevant terms during checking, than in the unifier, where hauling types around is a major overhead)

Awesome, thanks for the detailed reply! I did wonder about the types-in-semantics, and asked about it here: twitter.com/brendanzab/sta - nice to know that there is an alternative! cc.

@dannygratzer

Quote Tweet

· Nov 25, 2018

Replying to @dannygratzer

Linking back twitter.com/brendanzab/sta - yeah, for the neutral and normal forms.

GitHub - brendanzab/rust-nbe-for-mltt: Normalization by evaluation for Martin-Löf Type Theory with...

If I'm honest, it would be nice if you could make some of the identifiers longer and easier to read - part of what made mltt-for-nbe easy to get into was that it was more explicit. Although even then I tried to make things even clearer in github.com/brendanzab/rus 🙂

github.com

Normalization by evaluation for Martin-Löf Type Theory with dependent records - GitHub - brendanzab/rust-nbe-for-mltt: Normalization by evaluation for Martin-Löf Type Theory with dependent records

Stuff like `gApp` and `vInst` is hard for me to understand quickly, especially in lieu of comments. `Ix` is a misnomer, because its actually a DebBruijn level!