Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
summary
Automatic derivation of incremental type-checkers from Statix meta-DSL specifications uses scope graphs to turn name-resolution queries into precise inter-unit dependencies; a novel query-confirmation algorithm detects exactly which queries change after an edit so only affected compilation units reanalyze. The system splits type-checking into context-free and context-sensitive phases and reuses a generic mechanism for mutual dependencies. Prototype yields incremental type-checkers for any Statix spec and reports up to 147x speedup on synthetic benchmarks and 21x on real projects with initial overheads below 10%.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:36Overview
- 3:37Statix Rules
- 7:50Scope Graphs in Statix
- 9:45Problem & Solution Setup
- 11:08Verifying Queries
- 14:57Evaluation
- 17:32Conclusion
related talks
16mKnowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
46mThe Calculated Typer (Functional Pearl)
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
27mTowards Type Debugging using Partial Evaluation
34mIncremental Bidirectional Typing via Order Maintenance
23mIncremental compiler taming scalac
14mIncremental Bidirectional Typing via Order Maintenance