Implementing a dependent type-checker on optimal evaluators (HVM)

[VictorTaelin]

Hello. I've recently managed to implement a proper NbE on HVM, an optimal λ-calculus evaluator. By proper, I mean that any term that is reducible by HVM will be reducible by the corresponding NbE evaluator. This looks obvious, but isn't, because HVM, being based on the abstract algorithm, only admits a subset of the λ-calculus. Because of that, if the evaluator isn't designed with caution, it could happen that certain terms would be reducible on native HVM, but fail on its NbE. In special, the unquoting function must not perform any unnecessary cloning when converting a term to high order, which requires clever use of scope-less lambdas, and special care when manipulating the variable context. I've written details here.

Since smalltt relies heavily on NbE, and since we're now able to use NbE to run type-level computations directly on HVM (which is extremely fast, and often outperforms GHC on that kind of high-order terms), I believe we may push its performance even further. For example, by reading the README, I suspect some issues which you accounted for may not even apply:

if quoting returns full beta-normal terms, that reliably destroys performance

On the upcoming days, I'll be trying to bring some ideas of smalltt to build a dependent type-checker on HVM, and I'll let you know the results.