How to define exceptions in scheme using a dynamic variable and abortive control?

Question

I am having trouble implementing exceptions (handle and raise) using a dynamically scoped variable and abort.

This question came from reading the paper A syntactic theory of dynamic binding, section 6 figure 7.

What I have attempted seems to work correctly for throwing an exception inside a try block and also throwing an exception inside a try block inside a try block.

What doesn't work correctly is throwing an exception from inside a handler. It should abort to the next try block up in this case.

You can see my work here in racket scheme, along with 2 test programs. test-1 is working and test-2 is failing.

#lang racket

;; A Syntactic Theory of Dynamic Binding - Luc Moreau
;; https://link.springer.com/content/pdf/10.1007%2FBFb0030637.pdf

(require racket/control)

(define x_ed (make-parameter 'x_ed))

; NOTE: (abort ..) is the same as (shift k ..) where you don't use k
; NOTE: in (handle f M) we call f the handler and M the try block

; v1
;(define-syntax handle
;  (syntax-rules ()
;    ((handle f M)
;     (parameterize ((x_ed (lambda (v) (abort (f v))))) M))))
; v2
;(define-syntax handle
;  (syntax-rules ()
;    ((handle f M)
;     (reset (parameterize ((x_ed (lambda (v) (abort (f v))))) M)))))
; v3
;(define-syntax handle
;  (syntax-rules ()
;    ((handle f M)
;     (parameterize ((x_ed (lambda (v) (abort (f v))))) (reset M)))))
; v4
(define-syntax handle
  (syntax-rules ()
    ((handle f M)
     (let ((old-x_ed (x_ed)))
       (parameterize ((x_ed (lambda (v)
                              (abort (parameterize ((x_ed old-x_ed))
                                       (f v))))))
         (reset M))))))
(define-syntax raise
  (syntax-rules ()
    ((raise v) ((x_ed) v))))

(define (print x) (write x) (newline))

(define (test-1)
  (print "level-1 open")
  (handle (lambda (v)
            (print "level-1 caught"))
          (begin
            (print "level-2 open")
            (handle (lambda (v)
                      (print "level-2 caught"))
                    (begin
                      (print "level-3 open")
                      (raise #t)
                      (print "level-3 close")))
            (print "level-2 close")))
  (print "level-1 close"))

(define (test-2)
  (print "level-1 open")
  (handle (lambda (v)
            (print "level-1 caught"))
          (begin
            (print "level-2 open")
            (handle (lambda (v)
                      (print "level-2 caught")
                      (raise #t))
                    (begin
                      (print "level-3 open")
                      (raise #t)
                      (print "level-3 close")))
            (print "level-2 close")))
  (print "level-1 close"))

;v1
;> (test-1)
;"level-1 open"
;"level-2 open"
;"level-3 open"
;"level-2 caught"

;v2 and v3
;> (test-1)
;"level-1 open"
;"level-2 open"
;"level-3 open"
;"level-2 caught"
;"level-2 close"
;"level-1 close"

;v2 and v3
;> (test-2)
;...
;"level-2 caught"
;"level-2 caught"
; infinite loop

;v4
;> (test-2)
;"level-1 open"
;"level-2 open"
;"level-3 open"
;"level-2 caught"
;"level-1 caught"
;"level-2 close" <--- we don't want this to happen
;"level-1 close"

---

I was able to come up with this working version thanks to the answer:

(define-syntax handle
  (syntax-rules ()
    ((handle f M)
     (prompt0
      (parameterize ((x_ed (lambda (v)
                             (control0 k (f v)))))
        M)))))

Answer 1

(Edit: I was wrong about being able to make a more space-efficient implementation by using special control operators. It's possible to make the handler run in tail position with respect to the handle form, but I don't know of any way to evaluate the body in tail position too.)

First of all, are you specifically trying to implement exception handling where the body of a handle form is in tail position with respect to the handle form itself? If not, there are much more straightforward ways to implement exception handling in terms of simple escape continuations.

If you really want to implement "safe for space" or "properly tail recursive" exception handling, though, read on.

The challenge of implementing handle in a safe-for-space manner is that to avoid inserting an extra stack frame into the "no exception raised" path, you need the ability to unwind the stack and resume evaluation with an expression in that context. Or equivalently, resume evaluation by calling a procedure in that context. That is different from what call/cc provides; it only allows you to unwind the stack and then immediately return a value into that context.

You can simulate the extra power with call/cc at the cost of inserting an extra stack frame (so the body is not in tail position):

;; call/cc :       ((Any      -> None) -> Any) -> Any

;; call/cc/apply : (((-> Any) -> None) -> Any) -> Any
(define (call/cc/apply proc)
  ((call/cc (lambda (k) (let ([v (proc k)]) (lambda () v))))))

The extra stack frame comes from the application of the result of the call/cc expression.

Can you eliminate the need for that extra stack frame? Yes! But not with shift and reset.

The problem you ran into is that (abort e) (where abort corresponds to Felleisen and Hieb's A operator) is not the same as (shift _ e). If you look at the docs for shift and reset, you'll see the following reduction rules:

(reset val) => val
(reset E[(shift k expr)]) => (reset ((lambda (k) expr)
                                     (lambda (v) (reset E[v]))))
  ; where E has no reset

That is, shift does not remove its delimiting reset, and that stubborn reset is what prevents you from jumping out of your level-2 handler straight to your level-1 handler without running (print "level-2 close"). You need to pick a delimiter and a control operator that allows you to remove the delimiter.

You cannot do it with reset and shift.
You cannot do it with prompt and control.
You can do it with prompt0 and control0.
You can do it with % and fcontrol (and the right handler).
And of course you can do it with call-with-continuation-prompt and abort-current-continuation (and the right handler).