Datafun
Datafun is a new language I made with Neel Krishnaswami. It’s a simple, pure, and total functional language that generalizes Datalog. Datafun’s superpower is that it can concisely and declaratively express and compute fixed points of monotone maps on semilattices.
Here’s some further resources on Datafun:
Our ICFP 2016 paper introducing Datafun. You can also watch the recorded talk and its slides.
Video of my Strange Loop 2017 talk, and its slides.
Our POPL 2020 paper showing how to compute fixed points faster by incrementalizing the inner loop; this generalizes Datalog’s seminaïve evaluation. You can also see the recorded talk and its slides.
A mini-version of Datafun implemented in ~60 lines of Racket, with plenty of commented examples. Intended as a helpful introduction for folks who know Racket or Scheme. It includes set comprehensions and fixed points, but doesn’t handle monotonicity, semilattices, termination checking, or seminaive evaluation.
Incremental computation for faster fixed points
In late 2016 we began working on seminaive evaluation for Datafun: finding fixed points faster by incrementalising the iterated function. This work culminated in the POPL 2020 paper mentioned earlier. See also:
An extended abstract written for HOPE 2018.
Video of my talk at ICFP 2018 and its slides, and similar earlier slides from S-REPLS 5.
A three-page note proving a key result: the derivative of a fixed point is the fixed point of its derivative.
Modal types for monotonicity
In late 2017 we started work on a new, modal type system for Datafun that handles monotonicity more flexibly. See:
Video of my lightning talk at ICFP 2018 and its slides. Also a poster.
Video of my talk at S-REPLS 9 and its slides.
Unfortunately this work was never properly finished and published.