NbE type checking + conversion checking

(Andras Kovacs) #1

To address performance issues in Dhall, I think the most robust solution would be to switch from the current naive implementation of normalization and type checking to a modern one.

Recently, implementations of small type theoretic languages seem to converge on a similar design. Although AFAIK it does not have a canonical name, it is sometimes called “semantic type checking”, “Coquand’s algorithm” or “checking with normalization-by-evaluation”.

The basic idea was first described by Thierry Coquand. More recently, redtt, cubicaltt and the Pie language of the Little Typer book all build on this algorithm. Pie in particular is quite similar to Dhall in scope and features, and there is a detailed implementation tutorial for it. Also, Agda and Coq, while not explicitly based on Coquand’s algorithm, are much to closer to it than to Dhall.

In short about NbE-based checking:

  • There are two basic data types involved, one is usual syntax, the other one is a type of semantic values. Semantic values contain closures instead of binders, and they support efficient environment machine evaluation (which is usually similar operationally to GHC’s STG machine).
  • We go from syntax to values by evaluation and can go back from values to syntactic normal forms by quoting (synonym: readback). It is an important principle that no costly computation should transform syntax: the syntax is viewed as immutable machine code whose main purpose is to be evaluated into values, and instead we mostly compute on values.
  • This is in a sense just the replication of standard implementation practice in functional languages, where we have static immutable machine code, and runtime objects with closures in functions and thunks.
  • Type checking, evaluation and conversion checking always take place in an environment containing both types of binders, and also possibly values of their definitions.
  • No substitution or shifting is needed. Implementation is easier to get right and also much faster.

I implemented a new normalizer in this style for Dhall, which you can find in this pull request. So far, I only added a new-normalize option for the dhall executable, which can be used for testing and benchmarking, and the rest of the codebase is essentially unaffected. The new normalizer passed the normalization tests from dhall-lang.

My current impression is that

  • It would be possible and not super hard to switch implementation of type checking to NbE, without changing current Expr or semantics of normalization and type checking in any way.
  • Modest changes to Expr would yield additional performance benefits, but those are not as nearly as impactful as switching to NbE in the first place.

So far I’ve done relatively little benchmarking, the results are promising, but the real impact on user experience would be to have a new type checker and resolver, not just a standalone normalizer.

I’d be happy to hear about your thoughts. Additional testing and benchmarking for the new normalizer would also be nice, but I note that benchmarking is only possible now for import-free expressions (dhall new-normalize works like dhall normalize in this regard).

Performance improvements + interned identifiers