Provenance/Explanation

[saulshanabrook]

Hey! I am still getting up to speed on DD, so I apologize if this question is already answered somewhere, but I was curious if anyone has done any experiments adding provenance/explanation on top DD systems. I did see the work from about ten years ago here: https://github.com/frankmcsherry/explanation but was curious if anyone has extended that or are using that approach in a production system.

I work work on Egglog, a framework that can be used to build optimzers/compilers based on equality saturation and datalog. I am currently working with @oflatt to investigate ergonomic, performant, and modular ways to add proofs to a system like this. They are meant both for users to be able to understand why a certain equality holds in the end to help with debugging and also for verification of a result.

We are experimenting with porting egglog to different computational backends through this work, such as DD, duckdb, and souffle. One of the open questions is how to design a proofs system for a framework like this that can added in a modular manner, without baking it into the backend directly. We are trying out different implementations, including a source to source translation as well as more tightly integrated options to try to understand the performance, modularity, and maintainability tradeoffs between them, similar to work done for duckdb.

So as part of learning about the potential for a differential dataflow backend to egglog, I wanted to see if there are any best practices that have emerged around tracking provenance in a performant and modular manner. Appreciate any thoughts, thank you!

[frankmcsherry]

Hello! Not in production, but I'm currently trying to revive it for this stuff. The logic in the paper all checks out, worked great for DD at the time, it did rely strongly on DD's ability to handle non-monotonic computations. If you are in a monotonic Datalog (depending on what egglog reveals, I could see it being monotonic) you might get more mileage out of this paper for Datalog debugging. This was the intellectual antecedent of the DD work: use the rules of your language to track the derivations in your language.

My experience has been that DD really wins on expressivity compared to the other frameworks, and loses out for sure on at least every ergonomic dimension. It's more of an eDSL than a language, is tightly coupled to Rust, compiles really slowly, etc. The FlowLog folks put a more pleasant layer around it for Datalog, but my understanding from them is that they wish DD were easier to use, also. Not trying to scare you off, but do want to provide color.

Let me know if you have other questions. Happy to give my best shot at a fair read-out on the tools out there. I should be able to dig up the e-graph implementation in DD if that would help too! Might be you could get much of egglog into DD directly.

[saulshanabrook]

Thanks for all the pointers!

The interactive work looks really interesting... I wonder how hard it might be to implement egglog in it, either specialized on a particular program as an interpreter itself. Is the motivation here primarily around compile times or does it represent a different level of abstraction than the DD rust library?

I have to say that I don't know if the long compile times/Rust eDSL would really be a downside for egglog... Although I guess I won't know until I try if the compile times would be too much.

Happy to give my best shot at a fair read-out on the tools out there.

One thing that @ezrosent were talking about when we were looking into an egglog implementation framework was the DBSP work and in particular the Rust bindings. We thought maybe you might be a good person to ask on a perspective of the differences between the two for building something like egglog on? Are they just slightly different theoretical frameworks or is it clear where one is more useful than the other?

[frankmcsherry]

I really should be a good person for that, but I am not! I'm not super clear on the direction the DBSP work is headed, and at the time of my involvement, it was an opinionated restriction of DD. That restriction seemed to land pretty well, but I'm not clear on the specific motivation and direction (vs e.g timely + differential). But! I can summon @mihaibudiu and @ryzhyk and see if either of them have takes on the relationships between the bindings and direct differential usage. I'm keen to learn too, as it's not the first time it's come up.

[frankmcsherry]

The interactive work looks really interesting... I wonder how hard it might be to implement egglog in it, either specialized on a particular program as an interpreter itself. Is the motivation here primarily around compile times or does it represent a different level of abstraction than the DD rust library?

I suspect it wouldn't be that hard to do the e-graph part, in that it has a DD implementation (though .. with generic connected components rather than union-find). I'm less certain about the attached lattices with egglog though. Programming these in is less clear to me, unless there are a few baked flavor of lattice. The Flix connection is similar; lattice-valued aggregates work in DD (generally, semigroups; but lattices check out too), but programming the lattice join and meet functions in an interpreted language is where I stall out (at least, it calls for a second language).

I've had Claude take a swing at it a few times, as it is quite certain that egglog = e-graphs + abstract intepretation, which .. sounds great to me but I haven't entirely figured out yet. Tbh, I'm still coming up to speed on egglog and getting my head around the moments of great value (it took a while to grok e-graphs, so .. don't wait for me).

[mihaibudiu]

Both DBSP and DD are Turing-complete, so in principle you should be able to implement one on top of the other one.
Building DBSP on top of DD should be rather easy: you just promise always to supply deltas exactly in time order, advancing the time frontier after each delta. The other direction would take a bit of work. DD is clearly more general than DBSP.

What makes the two IMPLEMENTATIONS different is really trade-offs in the various implementation choices for operators, data structures, caching, concurrency, etc. For simple programs, DBSP may have a bit lower overheads: for example, the outer timestamps do not exist, they are always implicit.

Also, DBSP is really simple mathematically, whereas there's a handful of people who understand DD. I would argue that this makes DBSP easier to extend and use. Quite a few new implementations of DBSP are popping up, whereas I only know of one DD.

Rust compilation times depend a lot on the kinds of programs you write. The Feldera SQL compiler generates strongly-typed DBSP Rust programs from SQL, and these are a worst-case for the Rust compiler, e.g., Tuple128<A0, A1, ..., A127>.

[mihaibudiu]

Not sure if it's relevant or not, but https://github.com/brurucy/pydbsp is an incremental stratified Datalog interpreter implemented by @brurucy starting from the DBSP formalism which allows incremental changes to the Datalog program itself. This is all hand-written in Python, and uses a N^3 time lattice, so it's somewhere between DBSP and DD. The key observation is that you can build a Datalog interpreter using DBSP operators and you can express the program evaluation as a set of nested fixed-points.

[frankmcsherry]

Another direction you could head, though not nearly as buttoned up, is datatoad if you are interested in a lean datalog engine with WCOJ that just needs a bit of union-find sprinkled in. That could be a massive misunderstanding of egglog, of course, but .. datatoad is meant to be various forms of extensible, and seems to outperform many of the Datalog engines out there. I'd need to ramp up on exactly the edits to a Datalog system that egglog requires, but I could imagine it slotting in not unreasonably. Don't .. go too hard on that w/o me checking though; it could be a mess (no lattices at the moment, but nothing in the way of lattices other than typing).

[oflatt]

Super interesting thread!
We've been trying to figure out what exactly we actually need from a backend to run egglog efficiently.
A union find isn't actually a huge important part if you have a way to delete or subsume tuples. However, being able to run rules for a single iteration instead of saturating is very important