[tiarkrompf]

Sounds interesting. About the role of CPS: for specialization purposes, CPS can have some benefits by splitting control flow. For example, if your input is "if (c) a else b" and c is a staged (=symbolic) value, then a CPS interpreter can ignore the control-flow join that's implied by the if-then-else, and continue processing longer paths independently. However, this also quickly leads to exponential code blow-up, and hence, we do not use CPS for the core model described in the paper.

[phaedrus]

Thanks! The main application I'm looking at is logic programming, so the control flow example you give is apropos. For example a user function which requests A AND B could be written: "if not(A) then fail, else if not(B) then fail, else succ". The first time through, we might want to actually take every branch so that we learn about the whole expression. At this stage it's just building a graph that records edges between variables and constraints, so the exponential factor is averted.

However I keep going back and forth between having the user write logic in a "control flow" representation versus in a "declarative" way (e.g. "return A && B"). The declarative way expresses intent directly, but loses most of the hooks for stepping through in a callback. Expressing it as control flow on the other hand requires some form of custom control flow operators because the built-in ones can't be redefined in C++.

It turns out logical "OR" is very subtle because we want to "actually have taken" exactly one of the options, but we also don't want to fail contexts where the preconditions for both sides are satisfied; we actually just want to arbitrarily pick one (and then the other), but only one per run (except when we're reflecting).

Subtle things like that make me nervous as requirements the user's control flow logic has to abide by. So my main challenge is to either figure out constructs which make this foolproof, or come up with "nearly declarative" forms: code which expresses intent declaratively, but does so in multiple statements so that they can be single-stepped through.