[FEATURE REQUEST] Split e-graph & equality saturation into its own module

[tribbloid]

Is your feature request related to a problem? Please describe.

e-graph is an important infrastructure for compiler optimisation, are you interested in publishing your related work as an infra module, like egglog?

Once it become stable enough it can serve as an accelerator for various axiomatic rewrite systems (Scala 3 implicit search, Apache Spark SQL Catalyst optimiser, etc.). It can also be sharded using Apache Spark to enable distribute saturation and guided search.

Describe the solution you'd like

If you are interested, I can start working towards a minimalistic PR shortly.

Describe alternatives you've considered

The only Scala implementation I found is LISA prover, tho it will also take some effort to use & publish (https://github.com/epfl-lara/lisa/issues/226)

Additional context

The API of egglog-python can serve as a reference design specification. Comparing to the latest python, Scala is obviously less flexible but has more axiomatic reasoning capabilities. This can be played into our favour

[Bastacyclop]

Hi,

That sounds like an interesting project. I won't personally work on this, but a PR would be welcome if you manage to pull out the code into a separate repo linking back to this one.

Here are some concerns:

• The e-graph and equality saturation implementation of this repo is based on the Rust egg implementation, but has already drifted from the main branch of egg and its latest developments, how would you avoid this problem in the future? Beyond egg, will you reimplement egglog in Scala? Would it make more sense to create a Scala library that interoperates with the Rust libraries?
• Features specific to our Rise language needs are currently embedded into this implementation, that are not available in the generic egg Rust implementation, you'll have to think about how to become generic over these without breaking our use case.

I'm sure you've figured out where our eqsat code lives, but here is the folder: https://github.com/rise-lang/shine/tree/main/src/main/scala/rise/eqsat Some of this code includes features that I backported to generic egg in this repo: https://github.com/Bastacyclop/egg-sketches If you have questions on the code architecture, I am happy to answer them.

[tribbloid]

thanks a lot & congrats for being chosen by the legend (https://github.com/teorth/equational_theories)

I'll start by copying code into an independent Scala 2.13/gradle project and add generic type parameters, hoping that compatibility can be maintained while switching to a more scalable backend.

Upgrade to Scala 3 will be attempted in sync with shine compiler, though I can only hope that it happens fast.

Interacting with rust on diverse hardware architectures was a weak spot of JVM (it may be easier through FFI introduced in Java 22). But there are a few datalog implementations in Scala, some of them can even be distributed on many machines through Apache Spark.