A Typed Multi-Level Datalog IR and its Compiler Framework
summary
A compiler framework implements a typed multi-level Datalog IR in Scala, formalizing a bipolar, flow-sensitive type system with three-valued contexts that both enforces range-restrictions and tracks logic-variable bindings. The implementation integrates 4 Datalog frontends, 3 backends, and 16 IR extensions, lets one source program target different solvers for direct performance comparisons, and reduces frontend code size (examples: ~300 LOC for Soufflé, ~250 LOC for a functional language frontend, and a 10× reduction for a prior compiler).
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:25Datalog in PL research
- 3:14Datalog dialect challenges
- 5:22Typed multi-level Datalog IR
- 6:24Type system requirements
- 9:13Variable boundedness reasoning
- 11:21Bipolar type system design
- 13:29Polarity in type system
- 14:52Disjunctions and negation
- 15:57Compiler extensions
- 16:39Performance comparison
- 17:22Front end effort
- 18:02Summary
- 19:07Q&A: Prolog modes
- 19:49Q&A: Practical trade-offs
related talks
17mFixpoints for the Masses: Programming with First-Class Datalog Constraints
39mData-centric Metaprogramming
17mA Systematic Approach to Deriving Incremental Type Checkers
17mBring Your Own Data Structures to Datalog
41mHow types can turn a SQL interpreter into a SQL compiler
20mFunctional collection programming with semi-ring dictionaries
16mA Compiler for Fused Relational Operations on Multisets
17mInteractive Debugging of Datalog Programs