Hi everybody! I’m happy to announce that the first version of Metatheory.jl is out!
You can find the code here GitHub - 0x0f0f0f/Metatheory.jl
And if you want, you can read the introductory preprint here [2102.07888] Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation
But what is Metatheory.jl?
“Metatheory.jl is a general purpose metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern matching features.”
The package will be available in the Julia registry in 3 days, the mandatory waiting period. If you’d like to try Metatheory.jl, you can install it from the Github repository, as described in the README
There are a lot of possible use cases for Metatheory.jl : symbolic mathematics, compiler optimization, composable compiler transforms, theorem proving, program analysis, category theoretic algebraic computing, programming language interpreters.
I would be really happy to hear any kind of feedback and proposals, and to experiment with you in possible applications and use cases of Metatheory.jl . Please note that this package is still in a very early stage and I would not recommend you to start using it in production packages.
I would recommend, if you are planning to play and experiment with this weird new package, to read a bit about term rewriting, homoiconicity and metaprogramming, and particularly e-graphs. You may read more about our EGraph implementation in this paper by Max Willsey, distinguished at POPL21 and in these blogposts 1 2 by @Philip Zucker .
Feel free to open topics in the Metatheory.jl Zulip Stream
If you’d like to help in contributing to the project, please check out the CONTRIBUTING.md guide. There are a few things that need some works: we can optimize and make Metatheory.jl much faster, and we can investigate and experiment to see how to integrate the e-graph rewriting backend with Julia’s subtyping system and type lattice. One of the most requested features, was specifying and matching rules on the type of variables (symbols), and not only on the type of literal values. Another requested feature, really interesting to investigate, is attaching logical statements to expressions in the e-graph. Let’s experiment together find an elegant and efficient way of having these two killer features!