Implicit Incremental Type Checking

Aron Zwaan

Incremental analysis is of indispensable value for software engineers. They allow for real-time editor feedback, and minimal build times, even for larger projects in languages with complicated type-systems. In this talk, I will tell about my current research in providing implicit incrementality for type-checkers that use the scope graph theory for name resolution. This incrementality is based on two core ideas. First, we want to validate whether answers to queries from the previous result have changed, based on difference in the scope graphs. When answers are stable, we don’t need to restart the type-checker for a compilation unit, but instead we can reuse the result. Second, since this framework executes type-checkers concurrently, special attention to deadlock should be payed. Particularly, when the deadlock only contains unstarted units, we can immediately reuse all of their results, which saves a lot of computation time. Otherwise, we restart all currently unstarted units. In this way, we want to create reasonable execution times for Statix type-checkers, even for larger projects and specifications.

---

Previous: | Static Binary Translation of Concurrency
Next: Wouter Swierstra | A predicate transformer semantics for effects