I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs.
Is there an untyped $\lambda$-calculus extension that enables one to convert $\lambda$-terms into a form that can be syntactically manipulated and then subsequently evaluated?
I imagine that the calculus has two main additional terms:
- $\mathtt{reflect}\ v$: takes $v$ and produces a representation of $v$ amendable to syntactic manipulation.
- $\mathtt{eval}\ v$: takes a syntactic representation of a term and evaluates it.
In order to support reflection, a syntactic representation of terms is required. It would look something like:
- $\lambda x.e$ would be represented as a term $(\mathsf{LAM}\ R(e))$, where $R(e)$ is the reflected version of $e$,
- $e\ e'$ would be represented as term $(\mathsf{APP}\ R(e)\ R(e'))$, and
- $x$ would be represented as $(\mathsf{VAR}\ x)$.
With this representation, pattern matching could be used to manipulate terms.
But we run into a problem. $\mathtt{reflect}$ and $\mathtt{eval}$ need to be encoded as terms, as does pattern matching. Dealing with this seems to be straightforward, adding $\mathsf{REFLECT}$, $\mathsf{EVAL}$ and $\mathsf{MATCH}$, but will I need to add other terms to support the manipulation of these?
There are design choices that need to be made. What should the $R(-)$ function alluded to above do with the body of $\mathtt{reflect}$ and $\mathtt{eval}$? Should $R(-)$ transform the body or not?
As I am not so much interested in studying reflection itself -- the calculus would serve as a vehicle for other research -- I do not want to reinvent the wheel.
Are there any existing calculi that match what I have just described?
As far as I can tell, calculi such as MetaML, suggested in a comment, go a long way, but they do not include the ability to pattern match and deconstruct code fragments that have already been built.
One thing I would like to be able to do is the following:
- $\mathtt{let}\ x=\lambda y.y\ \mathtt{in}\ \mathtt{reflect}\ x \to (\mathsf{LAM}\ (\mathsf{VAR}\ y)\ (\mathsf{VAR}\ y))$
And then perform pattern matching on the result to build a completely different expression.
This is certainly not a conservative extension to the $\lambda$-calculus and the meta-theory is likely to be ugly, but this is kind of the point for my application. I want to break $\lambda$-abstractions apart.