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
Replying to
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. 🤔
Replying to
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
Show replies