Datafun

Datafun is a new language I’m working on 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:

Incremental computation for faster fixed points

Since late 2016 we’ve been 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:

Modal types for monotonicity

Since late 2017 I’ve been working on a new, “modal” type system for Datafun that handles monotonicity more flexibly. See: