I believe these ideas are much more mature and better explored for code gen, but similar techniques are useful also in the frontend of compilers, in the type ch

I believe these ideas are much more mature and better explored for code gen, but similar techniques are useful also in the frontend of compilers, in the type checker. There's a blog post [1] by Niko Matsakis where he writes about adding equalities to Datalog so that Rust's trait solver can be encoded in Datalog. Instead of desugaring equality into a special binary predicate to normal Datalog as Niko suggests, it can be also be implemented by keeping track of equality with union-find and then propagating equality through relations, eliminating now-duplicate rows recursively. The resulting system generalizes both Datalog and e-graphs, since the functionality axiom ("if f(x) = y and f(x) = z, then y = z") is a Datalog rule with equality if you phrase it in terms of the graph of functions. Systems implementing this are egglog [2] (related to egg mentioned in the article) and (self-plug, I'm the author) eqlog [3]. I've written about implementing Hindley-Milner type systems here: [4]. But I suspect that Datalog-based static analysis tools like CodeQL would also benefit from equalities/e-graphs. [1] https://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/ https://smallcultfollowing.com/babysteps/blog/2017/01/26/low... [2] https://github.com/egraphs-good/egglog https://github.com/egraphs-good/egglog [3] https://github.com/eqlog/eqlog https://github.com/eqlog/eqlog [4] https://www.mbid.me/posts/type-checking-with-eqlog-polymorphism/ https://www.mbid.me/posts/type-checking-with-eqlog-polymorph...