Bisimulation bleg

I have a question for anyone who happens to know: are bisimulations more common in process calculi such as the π-calculus because of τ transitions?

Lately I've been proving some simulation theorems for λ calculi, and none of them is a bisimulation; there are too many "administrative" reductions in the implementation semantics, so it's not possible to guarantee that every one-step reduction in the implementation semantics corresponds to a reduction sequence in the specification semantics.

Now, it's been a while since I looked at the π-calculus, but I seem to recall that you can hide a sequence of reductions inside a "black box" and call them a single transition τ. I suspect this facility allows you to pretend a sequence of transitions is a single transition in order to hide the details of an implementation semantics, effectively producing a completely indistinguishable simulation.

(This is admittedly all a little vague since my knowledge of bisimulations is scant.)

John Backus (1924 - 2007)

"The beauty of FORTRAN--and the reason it was an improvement over assembly language--is that it relieves the programmer of the obligation to make up names for intermediate results."
--Andrew Appel, Compiling with Continuations

My knowledge of the early history of programming languages is limited, but I believe Backus is considered to have invented the compiler. Slashdot unfairly describes Backus's Turing Award lecture "Can Programming be Liberated from the von Neumann Style?" as "apologizing" for the creation of FORTRAN, but I think the idea of functional programming was already there in FORTRAN. Once the idea of a FORmula TRANslator had been invented--i.e., the notion of a programming language with expressions--it was a natural step to consider languages without any statements at all.

This is to say nothing of the enormous debt of gratitude we owe him for BNF.

Update: Oh dear, I spoke too soon. Grace Hopper wrote the first compiler (thanks to the anonymous commenter for setting me straight). Apparently the FORTRAN compiler is considered one of the first successful optimizing compilers for a high-level language.

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.

Progress report

It's Saturday morning and I've had a full night's sleep--the first in a while and probably the last for a while. Progress report:

I've submitted my final paper on Space-Efficient Gradual Typing for the draft proceedings of Trends in Functional Programming with Aaron Tomb and Cormac Flanagan.

Now I'm working on several papers--one or two for ICFP and one for GPCE--and a couple of talks, all with deadlines in April.

Mostly

It occurred to me that my taste in programming languages tends to run in the "mostly" direction, such as mostly functional programming and mostly hygienic macros.

Avoiding coinduction in soundness proofs

Mads Tofte's thesis uses coinduction to prove type soundness for a language with a store, because of the problem of cycles within a store: if the value in a reference cell can point to itself (such as a closure that refers to the cell that contains it), then it's not possible to find the type of a value by looking in the store. That is, type soundness involves determining the type of values, and store addresses are one kind of value. If finding the type of an address means looking up its value in the store and finding the type of that value, but that value might itself contain the same address, then typing values is not inductive.

But according to Mitch and Matthias, it's not actually necessary to use coinduction, as long as you set up the soundness hypothesis right.

The statement of subject reduction usually looks like this:

For any type environment Γ, store typing Σ, expression e, and store σ, if

1. Γ;Σ ⊢ e : τ and
2. Γ;Σ ⊢ σ and
3. e,σ → e′,σ′

then ∃ Σ′ ⊇ Σ s.t.

1. Γ;Σ ⊢ e′ : τ and
2. Γ;Σ′ ⊢ σ′.

By quantifying over all stores in the hypothesis, you can get the value of an address by simply looking it up directly in the store typing, without passing through the actual value. So the definition of Γ;Σ ⊢ σ is

dom(σ) = dom(Σ)
∀a ∈ dom(σ) . Γ;Σ ⊢ σ(a) : Σ(a)
Γ;Σ ⊢ σ

and finding the type of an address value is defined simply by looking up the address in the store typing:

     (a : τ) ∈ Σ     
Γ;Σ ⊢ a : τ ref

Update: More accurately, the hypothesis that quantifies over all stores is in the main soundness theorem:

If ∅;Σ ⊢ e : τ and ∅;Σ ⊢ σ then either

1. e,σ diverges or
2. e,σ →* v,σ′ and ∃ Σ′ s.t. ∅;Σ′ ⊢ v : t and ∅;Σ ⊢ σ′.

The proof of this theorem is a straightforward induction over the length of the reduction sequence using progress and preservation. The interesting part is that it simply assumes from the outset that we have a store σ and a store typing Σ that agree. We can easily provide an initial store ∅ and store typing ∅, which trivially agree, to get the actual proposition we want as a corollary, namely that evaluating the program in the initial store produces a well-typed result.

Inkscape

Creating figures in LaTeX is a pain, especially if you want to embed LaTeX in your figures. In the past I've used xfig and pstricks, which allows you to embed typeset text in a diagram, but aside from all the hoops you have to jump through (I had to massage the output files before feeding them to TeX), what you see in the GUI is uninterpreted LaTeX source. So I was always nudging things over a pixel at a time, recompiling, and checking out the PDF.

This weekend I tried Inkscape, which has a more modern UI than xfig. From what I've seen so far it's pretty nice. It comes with a plugin that allows you to input a string of LaTeX source, and it creates a shell, compiles the LaTeX source, and uses pstoedit to convert the output to SVG to import back into your diagram. It's a hack, and a little slow, but it's true WYSIWYG again.

To get it to work in cygwin I had to tweak things a bit -- one very nice thing about Inkscape is that its extensions are just python source files stuck in a directory with a naming convention, which means I could tweak the file and rerun the command (without even restarting Inkscape!) and it would reload the plugin.

I created a script /usr/local/bin/tex2svg:

#!/bin/sh

base_dir=`cygpath -wl "$1"`
base_dir=`cygpath -u "${base_dir}"`

latex_file=$base_dir/eq.tex
aux_file=$base_dir/eq.aux
log_file=$base_dir/eq.log
ps_file=$base_dir/eq.ps
dvi_file=$base_dir/eq.dvi
svg_file=$base_dir/eq.svg
out_file=$base_dir/eq.out

latex -output-directory="${base_dir}" -halt-on-error \
  "${latex_file}" > "${out_file}" 2>&1
dvips -q -f -E -D 600 -y 5000 -o "${ps_file}" "${dvi_file}"

export LD_LIBRARY_PATH=/usr/lib/pstoedit:$LD_LIBRARY_PATH
pstoedit -f plot-svg -adt -ssp "${ps_file}" \
  "${svg_file}" > "${out_file}" 2>&1

The file $inkscape/share/extensions/eqtexsvg.py is the plugin; I commented out the lines that call latex, dvips, and pstoedit, and replaced them with a single command:

os.system("bash --login -e tex2svg '" + base_dir + "'")

Python and LaTeX were having all sorts of problems communicating about file names with different conventions (Unix, DOS 8.3, Windows long), so I just basically punted all the work to a shell script, where I could have better control over the file names via cygpath.

To use it, go to Effects | Render | LaTeX Formula, type in a LaTeX formula, and it will magically appear (after a few external windows blip on and off). I don't understand scaling issues, especially when you're dealing with multiple file formats (.tex, .dvi, .ps, .svg), but for whatever reason I've found that sometimes I have to kill the -y 5000 in the dvips command to get the right size.

Also, when I tried saving the diagram directly to PDF, it ended up kind of blurry. I've had better luck saving it to EPS. That means that you can't use pdflatex anymore; instead you have to use dvips followed by ps2pdf. But then they seem to look okay.

'a typing

There are a lot of typing paradigms running around these days without clear definitions. One of the difficulties is that any given phrase carries a number of different meanings, including (but not necessarily limited to) the phrase's apparent meaning from its constituent words, the phrase's common usage in any one of a number of different communities, the originator's intended meaning of the phrase, the original intended application domain of the paradigm, or the subsequent historical application domain of the paradigm.

Here's what I tend to mean by the following phrases. Disclaimer: I try to keep a balance between the aforementioned categories of meaning, although my community's common usage generally takes precedence. In any case there's a lot of vagueness and variability in the terminology, not to mention controversy. Read this at your own risk.

static typing: systems for reasoning about and enforcing inherent language invariants algorithmically and without involving program evaluation. In order to guarantee the invariants, the runtime semantics is only allowed to evaluate statically well-typed programs.

dynamic typing: systems for enforcing inherent language invariants incrementally during program evaluation via runtime checks.

soft typing: systems for detecting possible violations of imposed (i.e., not inherent) language invariants algorithmically and without involving program evaluation. The runtime semantics does not depend on programs being well-typed according to the soft typing algorithm.

optional typing: systems for detecting possible violations of imposed language invariants algorithmically and without involving program evaluation. The runtime semantics does not depend on program being well-typed according to the optional typing algorithm. (Come to think of it, I can't come up with a distinction between soft typing and optional typing off-hand.)

pluggable typing: systems of optional typing that admit any number of different static checking algorithms.

hybrid typing: systems for enforcing inherent language invariants algorithmically both via static reasoning and dynamic checks. This paradigm was originally introduced as a way to combine the static guarantees of statically typed languages with the more expressive annotation languages of dynamic contract systems.

gradual typing: systems for enforcing inherent language invariants algorithmically both via static reasoning and dynamic checks. This paradigm was originally introduced to facilitate program evolution by permitting incremental annotation of programs.

strong/weak typing: your guess is as good as mine.

Hello, I'm iTunes.

Apple can make fun of Vista's pesky security dialogs, but do you know what they make me do every time a sub-point release of iTunes is available?

1. iTunes asks me if I want to download the latest version.
2. I click yes.
3. Firefox opens to an ad-filled page with a form in the corner.
4. I uncheck the first "do you want us to email ads to you?" question.
5. I uncheck the second "do you want us to email ads to you?" question.
6. Here's a secret: if you uncheck both those boxes, you don't have to fill in an email address.
7. I click the "download" button.
8. Firefox asks me what to do with the file.
9. I click "Save file".
10. I wait for a thirty-five megabyte download, even if it's just a small patch.
    
11. I close the "Downloads" dialog box.
12. I close Firefox.
13. I close iTunes.
14. I find the downloaded setup executable.
15. I double-click the setup executable.
16. I click "Next".
17. I click "I accept".
18. I click "Next".
19. I click "Install".
20. I wait several musicless minutes for it to completely overwrite the entire existing installation directory, even if it's just a small patch.
21. Guess what, it still installs QuickTime on the side, as if I had any more interest in QuickTime than I have for the last 15 years.
22. I click "Finish".
23. iTunes starts (automatically! gee whiz!).
    
24. The license agreement pops up again.
25. I click "I Agree".
26. I wait a minute for iTunes to "update the iTunes library".
27. Here's the best part: as with every single previous release, iTunes still decides that maybe this time I really do want a QuickTime icon in the system tray.
28. I right-click the QuickTime tray icon and choose "QuickTime Preferences" (er, I prefer not to know about QuickTime?)
29. I click the "Advanced" tab.
30. I uncheck the "Install QuickTime icon in system tray" option at the bottom.
31. I click "OK".

And now I'm back to having iTunes working the way it did before. Only, as far as I can tell, the sole distinguishing feature of the new version is that it no longer asks me if I want to upgrade. For the moment.

Update: It looks like iTunes 7.0.2 installed a new "Apple Software Update" program on my computer. Does this mean my post was just in time to be obsolete? Here's hoping.

Hygienic typedefs

ECMAScript Edition 4 will have ML/C-style typedefs to allow the creation of type synonyms. You can think of these like macros in that, intuitively, references to such types are substituted by their definitions. This is simpler than a general macro system, because they are only substituting types in type contexts, not expressions in expression contexts. But even though types are a simpler subset of the syntactic structure of ES4 programs, due to generics, they still have binding structure!

Consider this example:

class C.<T> {
   type A = T
   function f.<T>() {
       var x : A = ...
   }
}

If we want to substitute away the type definition, we might naively get:

class C.<T> {
   function f.<T>() {
       var x : T = ...
   }
}

But then x's type annotation is referring to the wrong T! This corresponds exactly to the notion from hygienic macros (commonly referred to as referential transparency) that references in a macro definition should retain their meaning from the macro definition environment, never the macro use environment.

In other words, the above program should really be resolved to:

class C.<T> {
   function f.<T'>() {
       var x : T = ...
   }
}

Now consider another example, this time with a parameterized typedef:

type A.<X> = function.<T>():[X,T]
class C.<T> {
   var a : A.<T> = ...
}

A naive substitution would produce

class C.<T> {
   var a : function.<T>():[T,T] = ...
}

This time the bug is that we've allowed a type definition to introduce a binding that captured a binding in the context of the use of the typedef. This is an example of the hygiene condition, which states that bindings introduced by a macro should not capture variables in the macro application site. The proper expansion of the typedef would instead be:

class C.<T> {
   var a : function.<T'>():[T,T'] = ...
}

These are exactly the same conditions that hygienic macro expanders must meet in order to prevent unintended variable capture; the only difference is that here we're concerned with type variables rather than program variables.

A little goes a long way

I just completed an automated, machine-checked simulation proof. What was my proof assistant? Scheme! The proof relies on some reduction relations and an inductively defined invariant relation. The former can be defined in PLT Redex with just a little cleverness for performing symbolic reduction; the latter can be defined with good, old-fashioned recursion.

Granted, there are a number of places where I could have gone wrong. For example, I have no meta-theorems about the correctness of the representation or the exhaustiveness of the manually directed case analysis (a dozen cases in as many lines of code). But implementing the proof on the computer helped me debug a number of minor issues in my theorem, and it did all the heavy lifting for me (particularly the multi-step reductions--thanks Robby and Jacob for PLT Redex!).

The moral? A little goes a long way, as Wand and Sullivan wrote. For a simple proof involving inductive invariants and lots of rote calculation, there's no need for complicated meta-logical frameworks. Implementing the proof in a general-purpose programming language gives you a higher degree of quality assuredness for a reasonable implementation cost.

Next, if I do more of these simulation proofs, I might start abstracting out the common patterns into a library to work in conjunction with PLT Redex. It would essentially be a simple proof assistant for simulations.

Lazy substitutions

Substitution is expensive. That's why we tend to use environments in efficient implementations of programming languages. They encode all the information we need to do substitutions, but we wait until as late as possible to perform the substitutions. The complication, however, arises when expressions containing free variables (i.e., variables that haven't yet been substituted) travel around to disparate parts of the program. This happens in the lambda calculus when functions get passed or returned as values, and that's why we have to introduce closures. Closures allow expressions with free variables to travel around with enough information to continue performing their lazy substitutions.

In macro systems, we have exactly the same problem: the substitutions we need to perform (among others) are fresh names for bound variables. We need to substitute these fresh names throughout the bodies of expressions, but it's expensive to revisit syntax. So we close expressions over their substitutions and rename lazily.

But in macro systems, these kinds of closures are even more complicated than in the lambda calculus, because each macro invocation produces more code and mixes it together with other code. What we want is for the renamings to occur only on the code as it appears at the particular time of the current macro invocation. So in Dybvig, Hieb and Bruggeman's macro-expansion algorithm, the solution is to produce a fresh "mark" or "time-stamp" distinguishing code that resulted from a particular macro invocation. This way, renamings are applied only to code that existed at the time that the eager substitution would have been applied. When different code gets mixed together from different macro invocations, these marks keep track of what renamings apply to what pieces of syntax.

There are two salient features required of these marks: 1) every distinct invocation of a macro should have a distinct mark associated with it, and 2) only new code produced by a macro invocation should be marked as new, not code that it received as input. The first requirement is satisfied simply by generating fresh marks on each invocation. The second is satisfied by giving the mark algebra a "toggling" feature: re-applying the same mark twice to a piece of syntax erases the mark. The expander marks both the input and output of each macro invocation, which has the effect of "staining" new syntax generated by the invocation.

Symbolic evaluation with PLT Redex

PLT Redex is a great tool for testing and debugging a small-step operational semantics (particularly a reduction semantics using Felleisen-style evaluation contexts). I've just learned it's also useful for doing symbolic evaluation, where a program term may contain symbolic placeholders for some of its subterms. This is important when doing proofs, where you want to know how a fragment of a program is going to reduce for an entire class of terms.

For example, in a simulation proof I'm writing, I want to reason about how a program fragment would reduce in any initial continuation K0. So I extended the grammar of continuations to include the form

K ::= ... | (sym variable)

i.e., an s-expression containing the symbol 'sym followed by any variable. Then I could represent the abstract continuation K0 as '(sym K0). That's all it took, and Redex happily reduced my program.

Of course, once the reduction sequence gets to the point where it's returning a value to the continuation K0, it gets stuck, because there are no reduction rules that operate on these symbolic terms. But that's fine, because I'll never need to do such concrete reasoning about abstract terms.

Universal vs. existential properties of programs

There's an age-old debate about whether abstraction is an absolute necessity or an obstruction to programmer efficiency. It shows up in the static-vs.-dynamic typing war, the abstract datatypes-vs.-concrete representations war, etc. I've always suspected we'd be worse off if we let one side or the other win. Of course I don't claim to know how to resolve it, but I wonder if it would shed light on the issue to think about existential vs. universal properties of programs.

When you're debugging or testing code ("is it possible for this list to be empty?"), or when you're exploring an API at the REPL ("what happens when I pass the result of Foo to Bar?"), you're often looking to observe a single program trace that serves as a witness to an existential property. By contrast, when you're building robust systems, you often want to assert universal propositions about the code ("this function will only ever produce a non-negative integer").

When you're building a system, you want your invariants to be universally true. This is one place where enforcement of abstractions (as with static type systems) is important. Letting the software enforce the abstractions automates the process of verifying these properties.

When you're inspecting a system, though, you're often looking for particular, concrete examples. In my experience, people are better at going from the particular to the general rather than vice versa. I don't think we tend to think well in abstractions; at least not at first. That's why verifiers that work by searching for counterexamples produce such good errors: instead of directly proving ∀x.P(x), they try to prove ¬∃x.¬P(x), and if they fail, they give you a concrete x. Learning API's, interacting with the REPL, and writing test cases are all examples of this mode of programming where you're more interested in concrete paths through a program rather than universal properties.

How would we design software that facilitates both these modes of reasoning about programs?

Non-native shift/reset with exceptions, revisited

Filinski's implementation of shift and reset in terms of undelimited continuations and a mutable cell doesn't interact well with exceptions out of the box, but it turns out we can get the right behavior with only a slight modification. (Ryan, Jacob and I came up with this after John Reppy suggested it to me as a challenge that, if possible, would be far simpler to implement than a native implementation in SML/NJ.)

The problem is that, as Shan and Kiselyov point out, a delimited continuation should only close over the exception handlers (and dynamic parameters in general) bound up to its prompt, and when invoked, it should be invoked in the context of the handlers of the current global continuation extended by the handlers closed over by the delimited continuation. This really is the expected behavior; an exception raised in a delimited continuation should either be handled by an appropriate handler installed within the delimited context, or if there isn't one, by the global context in which the delimited continuation is being invoked.

For example, both of the following programs should evaluate to 100, since the exception inside the delimited continuation is raised within a new context that installs a handler for it:

;; handler installed in body of shift
(reset (lambda ()
         (+ (shift (lambda (k)
                     (with-handlers ([symbol? (lambda (exn) 100)])
                       (k 1))))
            (raise 'boo))))

;; handler installed in new context
(let ([k (reset (lambda ()
                  (shift (lambda (k) k))
                  (raise 'boo)))])
  (with-handlers ([symbol? (lambda (exn) 100)])
    (k 1)))

However, with Filinski's implementation applied naively to a language with exceptions, neither example manages to catch the exception because the delimited continuations close over the wrong exception handlers. However, we can get the right behavior with only a slight modification to the implementation. The trick is to modify the protocol between the captured Scheme continuations to pass an exception along from one context to another to be re-raised.

As before, we store the global continuation (or "meta-continuation") in the single mutable cell:

(define meta-k (lambda (x) (raise 'missing-reset)))

But we'll change the contract of the meta-continuation to accept two different variants of results, those representing a normal return from a delimited continuation, and those representing an unhandled exception that should be re-raised in the context of the meta-continuation's handlers:

(define-struct succeeded (result))
(define-struct failed (exception))

(This is the familiar pattern of representing different return paths in the exception monad.)

Now, reset needs to be modified to ensure that evaluation of the body of the prompt is wrapped in a handler to prevent uncaught exceptions from escaping to the original global continuation. The wrapped result is sent to the meta-continuation, and the context of the call/cc performs the unwrapping, either to return the ordinary value or re-raised the exception. (I've highlighted the new parts.)

(define (reset thunk)
  (let ([result
         (call/cc (lambda (k)
                    (let ([meta-k0 meta-k])
                      (set! meta-k (lambda (r)
                                     (set! meta-k meta-k0)
                                     (k r)))
                      (let ([v (with-handlers
                                   ([(lambda (exn) #t) make-failed])
                                 (make-succeeded (thunk)))])
                        (meta-k v)))))])
    (if (succeeded? result)
        (succeeded-result result)
        (raise (failed-exception result)))))

The only change to shift is that again, where it invokes the meta-continuation, it needs to wrap the result in this variant type. Because the meta-continuation is called here to represent the case where evaluation of the delimited continuation terminates successfully, we wrap the result with make-succeeded.

(define (shift f)
  (call/cc (lambda (k)
             (let ([v (f (lambda (v)
                           (reset (lambda ()
                                    (k v)))))])
               (meta-k (make-succeeded v))))))

That's it! Trying out the test cases above, we get 100 and 100, as we should.

This is also well-typed and implementable in SML, for example as a modification to Oleg's code.

POPL 2007 Program

I've found at least some version of all but two of the papers being presented at POPL next week. Here's a program with links to the papers I found.

Does type inference have to suck?

Type inference with tools like Haskell and SML obviously sucks. Hard. The error messages are useless. I have to pinpoint my errors manually, narrowing down the error by commenting out half the program at a time. Any time you're using binary search to find a bug, it's safe to say your debugging tools aren't helping you.

There's been a fair amount of pretty hardcore research on this. But does it really need to be hard? If I could just have some help from a modern IDE, it seems like type inference errors should be perfectly adequate. At the very least, the type inference engine could keep track of source location for every type constraint it acquires, and then when it finds conflicts, the GUI could simply draw an arrow between the two conflicting expressions. If it doesn't know which one is wrong, fine! I'll know which one is wrong, but it has to show me both!

SML/NJ's approach of picking one at random to blame is pure madness.

Another useful tool would be for the IDE to show me the inferred type of any expression in the program, so that if it's not manifest, I can at least make it manifest. Annotating one or two expressions at a time and recompiling is a colossal waste of time.

I've got plenty of criticisms for Eclipse, but if there's one thing we can learn from it, it's that compiled languages don't have to force the programmer into the edit-recompile cycle. It's perfectly possible these days to run the compiler incrementally and continuously. (Conversely, you could say that there's no reason why interpreted languages can't be incrementally compiled.)

I know I'm not the first to point this out. Why hasn't anyone in the statically-typed functional languages community done this? You don't need to reinvent the IDE, just build some plug-ins for emacs or Eclipse.

Dynamically optimizing dynamic dispatch

Robert O'Callahan just explained to me the basic optimization approach for dynamically typed languages that I've been hearing about lately. It's the approach used in the Strongtalk VM, recently mentioned by Avi Bryant and Gilad Bracha. At least, I think that's what they were talking about, but I didn't understand it until Robert explained it to me.

Performing a dynamic dispatch compiles into a branch deciding which class's method to invoke:

if (class == C) {
  C::foo();
}
else if (class == B) {
  B::foo();
}
else ...

With some runtime profiling, you can figure out which branch is most likely to occur and dynamically rewrite the branch so that the common case comes first in the branch.

if (class == B) {
  B::foo();
}
else if (class == C) {
  C::foo();
}
else ...

This then feeds into the hardware branch prediction.

With branch prediction, the hardware will keep some small history to help it predict which way to take. But if the particular branch in question is not in the history (say, because it's part of a loop with a large body whose branch history is bigger than the hardware branch history table), a conditional branch is an either-or; the branch predictor will still pick one. So as long as you structure the conditional so that the branch predictor will always guess the common path, even absent any branch history, it will still predict correctly in the common case.

This is something that you can't do with a vtable, because branch history tables are smaller for computed jumps (since each entry is a pointer rather than a single branch-taken/branch-not-taken bit), and because the hardware predictor can't guess right when it doesn't have a history.

You can then do even better by actually inlining the method body directly into the branching code, so it looks like

if (class == B) {
  // B::foo method body
}
else ...

and then even better, by merging several inlined methods in sequence. With some simple dataflow analysis on locals (between mutations), you can eliminate redundant checks. That is, code that looks like:

if (x.class == B) {
  // B::foo method body
}
else ...
if (x.class == B) {
  // B::bar method body
}
else ...

gets optimized to:

if (x.class == B) {
  // B::foo method body
  // B::bar method body
}
else ...

Non-native shift/reset with exceptions

Filinski's implementation of shift and reset has undesirable behavior in a language with exceptions. Consider the following example:

(reset (lambda ()
         (+ (shift (lambda (k)
                     (with-handlers ([symbol? (lambda (exn) 100)])
                       (k 1))))
            (raise 'boo))))

You'd expect this program to evaluate to 100, but with Filinski's implementation, it raises the uncaught exception 'boo. The same example with MzScheme's native delimited continuations yields 100.

Filinski's implementation of shift and reset

With the nice specification of shift and reset via local and global continuations, it's easier to understand Filinski's implementation in terms of a host language with undelimited continuations and mutable state. He uses a mutable cell to represent the global continuation:

(define meta-k (lambda (x) (raise 'missing-reset)))

The implementations of shift and reset push and pop representations of the local continuation onto this cell.

(define (reset thunk)
  (call/cc (lambda (k)
             (let ([meta-k0 meta-k])
               (set! meta-k (lambda (r)
                              (set! meta-k meta-k0)
                              (k r)))
               (let ([v (thunk)])
                 (meta-k v))))))

The reset function simulates pushing the local continuation onto the global one by updating it with a function that, when invoked, both pops the local continuation off (by simply mutating the global continuation back to its previous value) and jumps to the local continuation (by invoking the host language continuation captured by call/cc)--see the next-to-last eval rule. To ensure that the meta-continuation really does act like the global continuation, it is invoked on the result of the thunk; so even if the thunk never invokes a control effect, control eventually jumps to the initial global continuation.

(define (shift f)
  (call/cc (lambda (k)
             (let ([v (f (lambda (v)
                           (reset (lambda ()
                                    (k v)))))])
               (meta-k v)))))

The implementation of shift invokes its function argument and then forces a jump back to the global continuation afterwards--see the last eval rule. Even though the semantics suggests that the local continuation is immediately abandoned before evaluating the function argument, this implementation is morally equivalent; it doesn't bother to throw away the local continuation until after the function returns, but it still throws it away. The local continuation argument passed to the function argument is represented as a function that pushes the current local continuation onto the global continuation before jumping to the current local continuation--see the last cont1 rule.

Now, when taking into account proper tail recursion and space efficiency, this implementation is spectacularly wrong. Furthermore, stack reflection via language features like continuation marks will render this implementation inequivalent to native implementations of delimited control.