Specializing Scope Graph Resolution Queries: Extended Edition

TL;DR

This paper improves the performance of scope graph resolution in the Statix type system specification language by introducing a specialized partial evaluator, significantly reducing type checking time.

Contribution

It presents a novel partial evaluation approach and a tailored query language to optimize scope graph resolution in Statix, enhancing runtime efficiency.

Findings

Query resolution time improved up to 7.7x

Total type checking time reduced by 38-48%

Effective on benchmarks like Apache Commons CSV, IO, and Lang3

Abstract

To warrant programmer productivity, type checker results should be correct and available quickly. Correctness can be provided when a type checker implementation corresponds to a declarative type system specification. Statix is a type system specification language which achieves this by automatically deriving type checker implementations from declarative typing rules. A key feature of Statix is that it uses scope graphs for declarative specification of name resolution. However, compared to hand-written type checkers, type checkers derived from Statix specifications have sub-optimal run time performance. In this paper, we identify and resolve a performance bottleneck in the Statix solver, namely part of the name resolution algorithm, using partial evaluation. To this end, we introduce a tailored procedural intermediate query resolution language, and provide a specializer that translates declarative queries to this language. Evaluating this specializer by comparing type checking run time performance on three benchmarks (Apache Commons CSV, IO, and Lang3), shows that our specializer improves query resolution time up to 7.7x, which reduces the total type checking run time by 38 - 48%.