Just like Scheme... at first.
Error loads new meta level.
Notice the prompt change, from
The first number is the meta level, i.e. the n in metan level. The second number is just the iteration counter at this level.
Two ways to go back down.
(base-eval exp env cont).
Notice we needed to quote
inc at the meta-level. Why?
Let's jump back to the meta1 level and see.
We can jump levels normally with
exit, no need to fake errors.
Oh, we loaded meta2 now! Let's go back to 0:
To recap, a variable is local to a level:
Can we access some meta level without pushing away (or popping? which way does it go?) without leaving the level? Yes, with
Interesting, we got straight back to 0 from 3, some jumping indeed!
Each level in the tower has its own environment and continuation.
First, we redefine evaluation of variable (by mutating the meta
level) so that when the variable name is
_dummy we do
something special: we call the continuation first with
What happens when we evaluate
OK, so it seems that it just jumps out at the first
1? Not so fast:
If you'd like to learn more about semantics of reflective towers, including pushy vs. jumpy continuations, see the paper Intensions and Extensions in a Reflective Tower (PDF) by Danvy et al.
The loaded code in the examples below is also on Github.
Learn more about Church Encodings on Wikipedia. See also section 5.2 (Programming in the Lambda-Calculus) of Types and Programming Languages by Pierce.
There is a cute trick by Danvy et al.
extended journal version) to construct
(cnv xs ys) = (zip xs (reverse ys)) in
n recursive calls and no auxiliary data list, where
ys are lists of size
It's fun to think about it, so let's not give it away. Suffice to say that it's helpful to visualize the stack.
Happy Happy Joy Joy!