Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation
Alessandro Cheli · The Journal of Open Source Software · 2021
The Julia programming language is a fresh approach to technical computing (Bezanson et al., 2017), disrupting the popular conviction that a programming language cannot be high-level, easy to learn, and performant at the same time.One of the most practical features of Julia is the excellent metaprogramming and macro system, allowing for homoiconicity: programmatic generation and manipulation of expressions as first-class values, a well-known paradigm found in LISP dialects such as Scheme.Metatheory.jl is a general-purpose metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of its powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic patternmatching features.Intuitively, Metatheory.jl transforms Julia expressions into other Julia expressions at both compile time and run time.This allows users to perform customized and composable compiler optimizations that are specifically tailored to single, arbitrary Julia packages.The library provides a simple, algebraically composable interface to help scientists to implement and reason about all kinds of formal systems, by defining concise rewriting rules as syntactically-valid Julia code.The primary benefit of using Metatheory.jl is the algebraic nature of the specification of the rewriting system.Composable blocks of rewrite rules bear a strong resemblance to algebraic structures encountered in everyday scientific literature. SummaryMetatheory.jl offers a concise macro system to define theories: composable blocks of rewriting rules that can be executed through two, highly composable, rewriting backends.The first is based on standard rewriting, built on top of the pattern matcher developed in Zhao & Carlsson (2020).This approach, however, suffers from the usual problems of rewriting systems.For example, even trivial equational rules such as commutativity may lead to non-terminating systems and thus need to be adjusted by some sort of structuring or rewriting order, which is known to require extensive user reasoning.The other back-end for Metatheory.jl, the core of our contribution, is designed so that it does not require the user to reason about rewriting order.To do so it relies on equality saturation on e-graphs, the state-of-the-art technique adapted from the egg Rust library (Willsey et al., 2021).E-graphs can compactly represent many equivalent expressions and programs.Provided with a theory of rewriting rules, defined in pure Julia, the equality saturation process iteratively executes an e-graph-specific pattern matcher and inserts the matched substitutions.Since