When should I use Rosette's shallow vs. deep embedding for program synthesis?

Question

Some tutorials for Rosette introduce program synthesis using shallow embedding and others using deep embedding.

After reading Torlak et Bodik's "Growing Solver-Aided Languages with ROSETTE", it seems the shallow embedding is good for fast prototyping (since it does not require defining DSL & interpreter) and the deep embedding is good for making queries with stronger correctness guarantees. Is this a good rule of thumb for deciding which embedding to use?

What are good reasons for using Rosette's shallow vs deep embedding for program synthesis?

Answer 1

As a general rule of thumb, shallow embedding is best suited for applications that use the solver to search for values processed by a program, as is typical for program verification and angelic execution.

Deep embedding is the best choice if you are doing program synthesis and searching for (values that represent) code.

Shallow embedding can be a good choice for program synthesis if your application will be searching just for constants. But if you are searching for anything more complex (e.g., expressions or statements), deep embedding is the way to go.

With a shallow embedding, you have limited control of the space of programs that Rosette will search. Basically, you're limited to whatever can be encoded with Rosette's macro-based sketching constructs. These allow you to define basic search spaces and write quick prototypes, but if you want to build a tool that scales, you'll want tight control of the search space.

With a deep embedding, you have total control of the space of programs that will be searched. Essentially, you can write arbitrary Rosette / Racket functions to generate the symbolic program that represents all concrete programs to be searched. You then also have total control over the final step, which is code generation. Once Rosette returns a value (e.g., an AST) that represents a program in your deep embedding, you can process it however you want to generate code. With a shallow embedding, you are limited to using Rosette's built-in code generator.

So, to conclude, if you are doing or plan to do synthesis, use a deep embedding. For everything else (verification and angelic execution), shallow embedding will be easier and quicker.