Fixpoints for the Masses: Programming with First-Class Datalog Constraints
summary
Presents a concrete embedding of first-class Datalog constraints into a functional language, implemented as a 5k-line extension to the 60k-line Flix compiler, with a minimal lambda calculus, a Hindley-Milner style type system using row polymorphism, and a non-deterministic black-box solver model. Proves type safety (progress and preservation), supplies a compile-time stratified-negation check, and evaluates four case studies (three implemented: cones, an actor “puppet master,” and a configurable Python analysis) showing practical composition and modular rule inclusion; implementation is open source and ready to use.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:00Motivating Example
- 2:29The Problem But we now have two programs
- 3:29Proposed Solution
- 4:46Principles
- 5:13Type Safety: What can go wrong?
- 8:35Calculus
- 9:05Type System
- 11:25Stratification The Datalog program
- 15:40Case Study: Koan
related talks
01h 24mIntroduction to Constraint Logic Programming
17mBring Your Own Data Structures to Datalog
43mDatafun: a functional query language
52mI See What You Mean
21mA Typed Multi-Level Datalog IR and its Compiler Framework
36mOptimizing Relational Programs II
13mAccelerating Program Analyses in Datalog by Merging Library Facts
19mMaking Formulog Fast: An Argument for Unconventional Datalog Evaluation