Typechecker optimization

[Vtec234]

This issue is to discuss ideas for improving performance of the SynthLean typechecker, including both the time taken to check MLTT expressions and the sizes of the resulting typing derivations.

Performance curves on four benchmarks (fn/id/pair/prod) as of commit 88fc39d are reproduced below. We see that the time taken to typecheck a SynthLean term is superlinear in the time taken to typecheck the original Lean term for fn, pair, and prod, and that typing derivation sizes are superlinear in term size for fn and pair.

fn

id

pair

prod

[Vtec234]

• Firstly, we need to measure which parts of the checker (evaluation, equality checking, type synthesis) are taking the most time.
  • We should also inspect example typing derivations for signs of duplicated subterms or other inefficiencies. (Although we hash-cons these derivations, it is possible that some duplication remains, e.g. in the form of defeq-but-not-equal subterms.) If this turns out to be a real problem, we can manually let-bind terms that end up duplicated.
• Some speedup may come from reducing annotations on the syntax. This includes levels as well as types. Checking annotated syntax requires many more traversals than checking unannotated syntax would. We don't know to what extent this is alleviated by caching subterm traversals. Levels should be straightforward to remove (Get rid of level annotations on terms #119), whereas types are probably quite hard because the interpretation function needs them. There may be ways of doing 'bidirectional interpretation', or to prove an elaboration metatheorem.
• We run weak head normalization at various points in the checker, e.g. here. It may be possible to avoid WHNF by handling more defeq-but-syntactically-distinct cases.

[Vtec234]

Experiments in #165 demonstrate that performance is a critical issue.