Simple, pure, and total functional language that generalizes Datalog

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:

• Our github repository .

• Our ICFP 2016 paper .

• Video of my ICFP 2016 talk , and itsslides.

• Video of my Strange Loop 2017 talk , and itsslides.

• 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, or termination checking.

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. See:

• Anextended abstract written for HOPE 2018.

• Video of my talk at ICFP 2018 and itsslides, and similar earlierslides 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

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

• Video of my lightning talk at ICFP 2018 and itsslides. Also aposter.

• Video of my talk at S-REPLS 9 and itsslides.

• Notes-in-progress on the underlying theory .