I always want to see more on HN about programming languages and logic programming, but I'd like some context here, on the notability of the work that is presented in the linked article. It sounds cool. What are the current applications, uses?
Egg (and the e-graph theory behind it) has recently been put into use in some databases (e.g. cube[1]) and compilers (e.g. cranelift[2]). It lends itself well to the use-case of optimizing query planers and compilers, as it at the core avoids the optimization pass ordering problem (where an earlier optimization pass may destroy information that could be useful for a later one).
A more direct link to a list of applications of egraphs is https://egraphs-good.github.io/ Largely optimizing rewrites in compilers/synthesizers/query optimizer and theorem proving applications.
How does egglog compare to bddbddb, a Datalog engine powered by BDDs?
They use BDDs in Datalog to solve previously unsolved problems like context-sensitive pointer analysis for large programs and show that analyses implemented with it are faster than hand-tuned implementations and use dramatically fewer lines of code.
A small correction re: Cranelift -- I had originally prototyped with egg, but we're currently using a variant of egraphs I invented called "acyclic egraphs" after working through performance and productionization issues, with our own implementation. Egg is great for what it is; a production compiler is just a really particular and demanding environment. I'll be giving a talk about it at EGRAPHS 2023 (in the meantime there are details in the RFC you linked). E-graphs are cool! :-)
Related to equality-constrained tree automata[1], which (as far as I understand) can "pick" an implementation/realization out of a huge latent space of possibilities.
UW’s PL group has been focusing lately on this notion of E-Graphs and a technique called Equality Saturation. An E-Graph is a structure that efficiently represents equivalent rewrites of a program (exponentially many rewrites in polynomial space iiuc). Equality saturation is the process of generating an e-graph that represents all possible rewrites by inserting rewrites until the e-graph doesn’t change (is saturated). After the graph is created, you can use some heuristic to pick a good rewrite.
This paper applies E-graphs to augment Datalog's reasoning/constraint solving.
I'm just imagining a type system based on this. I've had ideas about a Datalog-based type system before, but it was never really practical; this could be the breakthrough that would make it practical!
