Performant Dynamically Typed E-Graphs in Pure Julia
summary
Metatheory.jl v3 implements e-graphs and equality saturation entirely in Julia, using a term interface that reads/writes expressions from byte buffers to support dynamic typing and dynamic multiple dispatch. Benchmarks show about 200x faster than the previous release, classical rewriting ~4× faster than Symbolics.jl, and performance that often reaches or exceeds egg (Rust) on standard EqSat workloads. It already supports extracting cost functions, source-to-source pattern macros, IR-level rewrites inside Julia compilers, and active CI benchmark runs on GitHub.
AI-written summary · about
chapters (15)
- 0:00Meth.jl and team intro
- 2:35Why Julia for e-graphs
- 4:17Meth.jl features
- 6:03Rewrite rules and workflow
- 7:48Dynamic typing in Meth.jl
- 9:38Julia’s dispatch and types
- 11:04Pattern matching in Meth.jl
- 12:50Benchmarks and speed
- 14:14Two-language problem solved
- 15:37Applications in Julia
- 17:24Optiflo and FPC optimization
- 18:05Future work and ecosystem
- 19:30Proof production in Julia
- 20:13Feature completeness and hiring
- 21:18Q&A
related talks
30megg: Fast and Extensible Equality Saturation
23mVersioned E-Graphs
22mJulia - Dynamism and Performance Reconciled by Design
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
17mBetter Together: Unifying Datalog and Equality Saturation
24mIncremental Equality Saturation
22mOatlog: A performant ahead-of-time compiled e-graph engine