Is egg a good foundation for a language based on term rewriting?

[ul]

I'm trying to understand the spectrum of egg use cases and wonder if it can be a basis for a language a-la https://agraef.github.io/pure-lang/ ?

[mwillsey]

(converted from issue #111 to discussion #112)

I think it is, in theory. Some other issues have brought up a similar question (#84). However, there are currently practicalities that make it difficult to pull this off without exploding the size of the e-graph. The most important issue is that the e-graph doesn't have any native support for binding. So you if you want to support a lambda calculus-like language, you have to resort to trickery like explicit substitution to support it. Right now, I think the performance cost of doing that is prohibitive to supporting "real" programming languages.

Note that egg is doing something more complicated that directed term rewriting. It's rewriting (potentially huge) families to other families, and doing this in parallel with other rewrites, all without "forgetting" the left-hand versions of any of those terms.

Supporting binding in the context of e-graphs and equality saturation is still an active research area, so hopefully this changes soon!

[Kesanov]

Couldn't you avoid the problem of free variables by using point free IR (e.g. similar IR to Forth)?

[mwillsey]

Sure! Encoding your language different makes all the difference! But it's still something that needs to be worked around.

[Kesanov]

Hm, so you are saying that Egg would be suitable as optimizer for Forth, or do you think that the size of the input (e.g. 10K LOC) would be too huge to make the performance competitive with existing optimizers?

[mwillsey]

It's possible, I haven't tried it 😀! One challenge I suspect you'd find is that if you have rewrites that re-order instructions or something, then egg will have a hard time. But maybe that can be avoided!