The last two weeks I've developed a demo implementation for high-performance type theory elaboration: github.com/AndrasKovacs/s. Performance gains are already huge.
Conversation
How does it compare to something like github.com/jozefg/nbe-for? I've been using this as a reference for my re-implementation of Pikelet's core. 🤔
1
2
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...
1
2
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
3
2
I could give detailed answers in other places, I'm not sure where, maybe on github.
2
2
(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)
1
Replying to
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.
Quote Tweet
Replying to @dannygratzer
Linking back twitter.com/brendanzab/sta - yeah, for the neutral and normal forms.
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 🙂
1
1
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!
1
Show replies