That is an interesting idea. I want to emphasize this point again:
"remember that an evaluation context is just a way of describing more
succinctly what you could otherwise define by hand as a big,
complicated relation on individual terms."
There is nothing special about evaluation contexts. I think they are
beautiful, but they don't, for example, automatically come with a set
of free theorems, like monads. The best thing they have going for them
is that they decouple the specification of evaluation rules and where
those rules occur (i.e. there are no "congruence" rules in the
reduction relation.) But, a reduction system can always have extra
rules that don't use them, so you don't get anything "for free". It is
possible that the thing you want can't be done using contexts, but
that doesn't mean redex or even redex's reduction-relation is wrong
tool to use.
That said, I don't think the idea of a "first-class" context or
evaluation rule makes sense, because the whole point of a proof theory
is to have a fixed set of proof schemas which you can reason about. If
you want to take term data and turn that into new rule cases, then
you'll have to have a more general rule that inspects the term data
and acts on it. For example, if you wanted your term data to be able
to cause evaluation anywhere, then one technique would be to by
default have evaluation happen everywhere, but then the evaluation
rule will inspect the context to see if evaluation is enabled in any
specific case. I think that makes sense from an implementation
perspective too.
Maybe not useful, but I believe that delimited control was really made
by Matthias to solve the same problem as algebraic effects are solving
today. Read his papers again in that light and it may be helpful. I
have a series of blog posts from 2012 that attempt to explain this
perspective [1] through [2] and this is how my DOS package works [3].
DOS makes this really explicit because the state outside of the
handlers is specified as a monoid that combines the effects from each
of the contexts that can create effects.
Jay
1.
https://jeapostrophe.github.io/2012-06-18-pipe-post.html
2.
https://jeapostrophe.github.io/2012-07-12-cont-sys-post.html
3.
https://docs.racket-lang.org/dos/index.html