Split e-graph & equality saturation into its own module

[tribbloid]

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.

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

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

[SimonGuilloud]

Hi! it would be interesting to do yes. I had in mind maybe writing a generic e-graph implementation (maybe for the scala3 collections library). I'm pretty sure that it should be possible using higher-kinded types. Would that correspond to what you have in mind? I have read the egglog paper in the past, but never used the tool itself.

[tribbloid]

the original egglog-rust API is very verbose, egglog-python is much better:

# @egraph.class_
class Dim(Expr):
    """
    A dimension of a matix.

    >>> Dim(3) * Dim.named("n")
    Dim(3) * Dim.named("n")
    """

    def __init__(self, value: i64Like) -> None:
        ...

    @classmethod
    def named(cls, name: StringLike) -> Dim:
        ...

    def __mul__(self, other: Dim) -> Dim:
        ...

The ellipse part will be filled by the library to construct new expression. In Scala eta-reduction can kind of enable an equally laconic API without losing type safety.

I've also read the rise compiler implementation (from the author of guided EqSat https://dl.acm.org/doi/10.1145/3632900). This is my impression of its capabilities so far:

• strongly typed: every ENode/EClass has an associated type that verifies assignment, they are always enabled in every universe
• primary universe is hyper-optimised for the compiler, with all existing expressions mapped from SIMD operators. I don't see much use of higher kind, if any.
• 2nd universe is built for pattern matching and structural search
• guided EqSat capability is enabled through sketch definition which relies heavily on the 2nd universe
• it is written in Scala 2.13, oops (maybe Apache Spark maintainer will appreciate it, but I don't).

the guided EqSat & sketch capability appears to be important enough to be included in some of the most hairy proofs (e.g. https://github.com/teorth/equational_theories). So I'm inclined to include it as a core feature.

Perhaps I can negotiate for a list of core features on his behalf?