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.