If I remember correctly, you (the author/implementor of Cammy) have used egg (or another backend for equality saturation), and also RPython (Pypy’s machinery for self-optimizing interpreters). I would be curious about what your experience was with using these two advanced tools.

Yes, Cammy’s toolchain uses both of those ingredients.

egg is reasonably well-implemented. I did not grok the algorithm for a long time, and I initially wrote a basic and slow version in Monte just to understand it. One of the design choices in Cammy is to avoid binding names, so that alpha-equivalence is trivial. As a result, the egg optimizer for Cammy does not need any name management and can use egg’s builtin demonstration language for symbolic manipulation.

RPython has an incredible power-to-effort ratio among JIT toolkits. The only comparable system is Truffle/Graal, whose owners unfortunately are notoriously untrustworthy Oracle. RPython has cryptic error messages during translation, but otherwise behaves like Python 2.7 . JIT output is controlled by minimal inline annotations, and improved by altering plain Python code and using high-level algorithmic analysis. Even the JIT optimizer’s output is human-readable and high-level. The current cammy-run JIT is around 500 lines of RPython implementing a basic AST interpreter, and it is faster for my purposes than AOT compilation with OCaml or CHICKEN Scheme.

Thanks for your nice reply. Looking at your egg rules, it looks like the vast majority of them are simple rewrite-rules (linear left pattern) that are obviously terminating: it gives the impression that the full power of equivalence-checking is not needed to simplify those. (But I guess egg performs well there as well.) The exceptions I can see is that you gave both composition-reassociation orders (does it work measurably worse with just one of them?), and the case-* and pair-* rules which use equality checking on their input.

One of the design choices in Cammy is to avoid binding names, so that alpha-equivalence is trivial.

On the other hand, using categorical combinators for functions/exponentials means that you have De-Bruijn-like notations for higher-order functions (I would expect them to show up as repeated fst applications to get far-away arguments of currified functions), and in particular it is not trivial to determine that two subterms are in fact equivalent: (fun x -> y) and (fun x -> y), for the same variable y, may be written differently depending on the number of function-bound variables between the definition of y and their occurrences.

I’m not sure if that would be an issue in practice, or if systematic local rewriting magically makes these issues go away. It looks like you have mostly written first-order programs for now, so this is difficult to tell by looking at examples.

So far, the rules needed have been very simple, and hopefully that will always be the case. But if I need more flexibility or power, I hopefully can write more Rust. Among the nice features of egg is a scheduler for rewrites, so that including the rules for associativity of composition does not overwhelm the time spent searching for improvements.

So far, I haven’t had any serious ergonomic issues with higher-order functions. I have had to stop for a moment and figure out which projections I need from a nested tuple, but it has not been the hard part. The hard part has been dealing with totality. For example, I could not figure out how to unfold a list for a couple weeks, because the traditional formulas are unbounded. I had to implement a bounded unfold instead.

If I remember correctly, you (the author/implementor of Cammy) have used

`egg`

(or another backend for equality saturation), and also RPython (Pypy’s machinery for self-optimizing interpreters). I would be curious about what your experience was with using these two advanced tools.Yes, Cammy’s toolchain uses both of those ingredients.

egg is reasonably well-implemented. I did not grok the algorithm for a long time, and I initially wrote a basic and slow version in Monte just to understand it. One of the design choices in Cammy is to avoid binding names, so that alpha-equivalence is trivial. As a result, the egg optimizer for Cammy does not need any name management and can use egg’s builtin demonstration language for symbolic manipulation.

RPython has an incredible power-to-effort ratio among JIT toolkits. The only comparable system is Truffle/Graal, whose owners unfortunately are notoriously untrustworthy Oracle. RPython has cryptic error messages during translation, but otherwise behaves like Python 2.7 . JIT output is controlled by minimal inline annotations, and improved by altering plain Python code and using high-level algorithmic analysis. Even the JIT optimizer’s output is human-readable and high-level. The current cammy-run JIT is around 500 lines of RPython implementing a basic AST interpreter, and it is faster for my purposes than AOT compilation with OCaml or CHICKEN Scheme.

Thanks for your nice reply. Looking at your egg rules, it looks like the vast majority of them are simple rewrite-rules (linear left pattern) that are obviously terminating: it gives the impression that the full power of equivalence-checking is not needed to simplify those. (But I guess egg performs well there as well.) The exceptions I can see is that you gave both composition-reassociation orders (does it work measurably worse with just one of them?), and the case-* and pair-* rules which use equality checking on their input.

On the other hand, using categorical combinators for functions/exponentials means that you have De-Bruijn-like notations for higher-order functions (I would expect them to show up as repeated

`fst`

applications to get far-away arguments of currified functions), and in particular it is not trivial to determine that two subterms are in fact equivalent:`(fun x -> y)`

and`(fun x -> y)`

, for the same variable`y`

, may be written differently depending on the number of function-bound variables between the definition of`y`

and their occurrences.I’m not sure if that would be an issue in practice, or if systematic local rewriting magically makes these issues go away. It looks like you have mostly written first-order programs for now, so this is difficult to tell by looking at examples.

So far, the rules needed have been very simple, and hopefully that will always be the case. But if I need more flexibility or power, I hopefully can write more Rust. Among the nice features of

`egg`

is a scheduler for rewrites, so that including the rules for associativity of composition does not overwhelm the time spent searching for improvements.So far, I haven’t had any serious ergonomic issues with higher-order functions. I have had to stop for a moment and figure out which projections I need from a nested tuple, but it has not been the hard part. The hard part has been dealing with totality. For example, I could not figure out how to unfold a list for a couple weeks, because the traditional formulas are unbounded. I had to implement a bounded unfold instead.