Saturday, March 10, 2007

Inside-out evaluation contexts

I've been a big fan of the "inside-out" (i.e., zipper) formulation of evaluation contexts, but almost everyone I talk to has a real problem with it. I think this is primarily due to lack of familiarity, but I do recognize that it requires you to stand on your head.

I'd thought for a while it was the only real way to specify evaluation contexts for a CEK machine semantics, but in fact it's really only an optimized representation for that approach. The outside-in definitions work just fine.

All you need in a CEK machine is to be able to match the innermost frame of a context by decomposing it into E[F]. With the inside-out formulation, frames are stacked up from inside out, so this is tantamount to looking at the head of a list. This is so efficient that the entire history of stack-based language implementations uses it. However, it's still possible to match E[F] with the inside-out outside-in formulation, it just requires recursively traversing the context until you find the innermost frame F.

I think I'll probably stick with outside-in for most of my papers, since it seems to generate so much angst.

Update: whoops! corrected a typo.


KSM said...

I think I'll probably stick with outside-in for most of my papers, since it seems to generate so much angst.
No! Don't do it!

Or at least, not for that reason. The only way inside-out will stop causing angst is if readers get used to seeing it.

Outside-in is really just a historical accident. In addition to corresponding exactly to abstract machine contexts (thus, defunctionalized continuations), inside-out makes both decomposition into a context and redex and plugging a term into a context tail recursive.

Neel Krishnaswami said...

Can you avoid the angst by just calling your continuation a "stack" instead of an "evaluation context"? And then write about "pushing things on the stack", and you've slipped them their medicine with a spoonful of implementation. :)

KSM said...

Well, Andy Pitts calls them "frame stacks", composed of "frames" in his Parametric Polymorphism and Observational Equivalence stuff, so I guess one *could* call them stacks.

I would say though, that with Matthias as an advisor, *Dave* will not be able to avoid angst by calling them stacks.

jto said...

Well, it threw me for a loop, but I'm not well-read in PLT.

It only dawned on me a few minutes ago that the enumeration of Evaluation Contexts was not just a repeat of the entire grammar, but a select subset, chosen to constrain the order in which reductions happen.

I didn't make the connection between "evaluation context" and "continuation" either, but it seems quite obvious now.

icosahedron said...
This comment has been removed by the author.