# 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:

Video of my ICFP 2016 talk, and its slides.

Video of my Strange Loop 2017 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, 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:

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: