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.
The intro is nice and easy and then it really jumps into some detailed PL theory that I couldn't quite grok. why do papers so often do this? start like a leisurely stroll and-BAM! "discrete comonads". Guess as a non-expert I'm not quite the target audience.
Yeah cat theory jargon always makes me gape. I should revisit some of Spivak’s work directed at teaching cat theory to programmers, if only to know how this thesis does what it does.
> 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.
Thanks for sharing the summary. There's also this Strange Loop 2017 talk "Datafun: a functional query language" with an early overview of this research: https://www.youtube.com/watch?v=gC295d3V9gE
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.
7 comments
[ 2.5 ms ] story [ 28.6 ms ] thread> 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.