A Systematic Approach to Deriving Incremental Type Checkers
summary
Provides a compiler from textbook-style typing rules to Datalog that yields an incremental type checker and a DSL for language specs, with a concrete encoding that decomposes typing into a context-passing relation and a type-of-expression relation, then replaces context lookup with a synthesized find relation and adds an error collection relation to avoid cache oscillation. Microbenchmarks show up to 13000x speedups for low-impact edits, initial 1.4–7x slowups for big edits improved to 7–900x after optimizations, at the cost of ~6x slower initialization.
AI-written summary · about
chapters (8)
- 0:00Motivation for the project
- 0:40Using datalog for typing
- 2:20Overcoming finiteness limits
- 5:47Encoding the type relation
- 7:31Initial performance analysis
- 8:42Optimizing sub-optimal cases
- 12:33Improved performance results
- 14:25Future work and summary
related talks
15mIncremental Processing of Structured Data in Datalog
21mA Typed Multi-Level Datalog IR and its Compiler Framework
36mData Driven UIs, Incrementally
26mStateful Differential Operators for Incremental Computing
17mInteractive Debugging of Datalog Programs
17mBetter Together: Unifying Datalog and Equality Saturation
24mA Counterexample-Guided Debugger for Non-Recursive Datalog
17mBring Your Own Data Structures to Datalog