Incremental type-checking for free: using scope graphs to derive incremental type-checkers
Aron Zwaan, Hendrik van Antwerpen, Eelco Visser
Abstract
Fast analysis response times in IDEs are essential for a good editor experience. Incremental type-checking can provide that in a scalable fashion. However, existing techniques are not reusable between languages. Moreover, mutual and dynamic dependencies preclude traditional approaches to incrementality. This makes finding automatic approaches to incremental type-checking a challenging but important open question.
In this paper, we present a technique that automatically derives incremental type-checkers from type system specifications written in the Statix meta-DSL. We use name resolution queries in scope graphs (a generic model of name binding embedded in Statix) to derive dependencies between compilation units. A novel query confirmation algorithm finds queries for which the answer changed due to an edit in the program. Only units with such queries require reanalysis. The effectiveness of this algorithm is improved by (1) splitting the type-checking task into a context-free and a context-sensitive part, and (2) reusing a generic mechanism to resolve mutual dependencies. This automatically yields incremental type-checkers for any Statix specification.
Compared to non-incremental parallel execution, we achieve speedups up to 147x on synthetic benchmarks, and up to 21x on real-world projects, with initial overheads below 10%. This suggests that our framework can provide efficient incremental type-checking to the wide range of languages supported by Statix.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Builds on4
- Incremental whole-program analysis in Datalog with latticesTamás Szabó, Sebastian Erdweg, Gábor BergmannPLDI 2021 · 39 citations
- A systematic approach to deriving incremental type checkersAndré Pacak, Sebastian Erdweg, Tamás SzabóOOPSLA 2020 · 16 citations
- Language-parametric static semantic code completionDaniël A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco VisserOOPSLA 2022 · 10 citations
- Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specificationsArjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers et al.OOPSLA 2020 · 9 citations
Related papers
- Language-Parametric Reference SynthesisDaniël A. A. Pelsmaeker, Aron Zwaan, Casper Bach Poulsen, Arjan J. MooijOOPSLA 2025 · 1 citation
- Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and RocqThomas Lamiaux, Yannick Forster, Matthieu Sozeau, Nicolas TabareauPLDI 2026
- Differential Execution with Lexical TracingSebastian Erdweg, Runqing Xu, Mo BitarOOPSLA 2026
- Incremental Certified ProgrammingTomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric TanterOOPSLA 2025
- Incremental Bidirectional Typing via Order MaintenanceThomas Porter, Marisa Kirisame, Ivan Wei, Pavel Panchekha et al.OOPSLA 2025 · 2 citations
