Deconstructing Datalog [pdf]

> if we were to distill this dissertation into their key ideas, it would be these:

> Model monotonicity with modal types. Datalog can be summarized as relational algebra plus stratified recursive queries. Modulo implementation subtleties, relational algebra embeds straightforwardly in a functional language via finite sets and set comprehensions. We have shown that stratified recursive queries also embed nicely, so long as we locate our semantics in Poset to capture compositional reasoning about monotonicity. The main difficulty is the interaction of monotone and non-monotone functions; this arises from the discreteness comonad □, and can be handled with a simple modal type system.

> To find fixed points faster, incrementalize! Finding a fixed point by iteration involves repeatedly changing a function’s input to match its changing output. Doing this naïvely is asymptotically inefficient; to do it efficiently, we must efficiently propagate changes. This is not only the essence of seminaïve evaluation in Datalog, but an instance of a greater problem of automatic incremental computation. Prior work on the incremental λ-calculus shows that incremental computation can be achieved in higher-order languages; we have extended it to Datafun and shown that by modifying it to consider only increasing changes, it gives rise to seminaïve evaluation.

I only read the first section on monotone fixed points. A real pleasure. Nothing new, but the key ideas explained in simple yet precise terms and examples. It really makes me want to read more.

I saw the Datafun presentation at Strangeloop some years back, so it’s really cool to see these ideas come to such an impressive fruition. In the meantime, a virtual machine for an RDF based logic language became my own side project/obsession, so this dissertation looks like exactly what I need.