Incorrect types for call-with-exception-handler

[cloudrac3r]

(1) This should work but doesn't, with an unhelpful error:

#lang typed/racket/base
(: example-1 : -> Void)
(define (example-1)
  (call-with-exception-handler
   (λ (e)
     (println "the handler")
     e)
   (λ ()
     (println "the message"))))

(2) This could be better:

#lang typed/racket/base
(define (example-2)
  (call-with-exception-handler
   (λ (e) e)
   (λ ()
     (+ 2 2))))

> example-2
- : (-> Any) ;; this would be more accurate as : (-> Positive-Index)

I can fix this with this, which seems sound:

(require/typed/provide racket/base
  [call-with-exception-handler (∀ (A) ((Any -> Any) (-> A) -> A))])

I don't understand the syntax of base-env.rkt so I'm not sure how to PR this fix myself.

[samth]

Can you say more about why you're confident this is sound? This is a fairly tricky area of Racket semantics where it's easy to make mistakes.

[cloudrac3r]

I'm not sure what exactly you want me to explain regarding soundness, because I don't think the code is particularly complicated. It's just a matter of copying the contracts in the docs to types. So I'll explain how I did that.

First argument is the exception handler which takes the exception and returns an (optionally modified) exception to be raised. But according to the docs these can be any values, not just exceptions, because I guess this is a fairly low level operation. So, that makes the (Any -> Any) argument.

Second argument is the thunk which will be executed with the handler around its dynamic extent. This takes no arguments and according to the docs may return multiple values. Whatever it returns becomes the return value of call-with-exception-handler. So, that makes the (∀ (A) (-> A) -> A) argument. It makes the inner return type, whatever it may be, match the outer return type.

Put those together and you get the fix in my original post, and if you paste that in the same file as the examples, they work properly instead of not working.

I don't see any gotchas here. Is there something I'm overlooking?

[cloudrac3r]

Based on my experimentation, the current built-in types have call-with-exception-handler as always returning Any, which is definitely incorrect and was making my code not compile. example-1 is a minimal reproducible example of that code.

If I'm reading base-env correctly, they appear to have a generic on the handler function making its input type match its output, which would also be incorrect.

[samth]

The issue is that you can't just copy contracts in the documentation to types. The contracts in the documentation are (a) informative for reading and (b) don't fail -- they don't make stronger promises than that. In the case of call-with-exception-handler they only say that the f argument is a function of one argument, the thunk argument is a function of no arguments, and that's it. The documentation doesn't make any promises about what the results of those functions has to be, or about what the overall result of the call will be (that's what any as a result contract means).

I think, from reading the docs for call-with-exception-handler and for uncaught-exception-handler that there's no way to produce any results from call-with-exception-handler other than the result of thunk. But I worry a bit that it might be possible to, for example, produce a result from f, either by returning a value or by raising an exception, that would put a result in as the result of call-with-exception-handler. So I'm hoping that you've thought this through for your code.

[cloudrac3r]

I barely understand continuations, but looking at the Racket internals, I think it's fine - anything from f is raised and not returned. First, a continuation is marked with exception-handler-key associated with f, and thunk is evaluated. Only if an exception is raised does f execute, which is done by the usual do-raise mechanism, which calls all exception handlers in order, passing each return value from one as the argument to the next. This isn't able to return a value to the original thunk after f has been called.

So the overall return value is either the return value of thunk, or it never completes due to a raised exception.

[rfindler]

I think that the formal semantics in the r6rs covers this construct if I am not mistaken? It has been a while tho. 😄

[cloudrac3r]

I am no longer confident this is sound.

[samth]

Interesting, can you say more? I spent some time thinking about it and couldn't come up with a hole.

[cloudrac3r]

My real-world use case was to write a data structure to a file, and if there is an exception during the writing process (due to finding something it can't handle while walking the data structure) to clean up by deleting the file, which would otherwise remain partially written on disk. Here's reproduction code for that:

#lang typed/racket/base
(require/typed/provide racket/base
  [call-with-exception-handler (∀ (A) ((Any -> Any) (-> A) -> A))])

(define file-name "test.txt")

(define (create-content #:fail? [fail? #f])
  (displayln "wa")
  (when fail?
    (error 'create-content "asked to fail"))
  (displayln "finished writing"))

(call-with-exception-handler
 (λ (e)
   (delete-file file-name)
   e)
 (λ ()
   (with-output-to-file
     #:exists 'replace
     file-name
     (λ ()
       (create-content #:fail? #f)))))

#:fail? #f writes the whole file without errors and you can check it.
#:fail? #t simulates an error partway through writing the file.

The intention is that the first function of call-with-exception-handler should notice the error, delete the file, and then pass up the error to the rest of my error handling/reporting code.

In Typed Racket with my proposed require/typed/provide, I get this:

; exception raised by exception handler: call-with-exception-handler: broke its own contract
;   Attempted to use a higher-order value passed as `Any` in untyped code: #<continuation-mark-set>
;   in: the range of
;       a part of the or/c of
;       the 1st argument of
;       (parametric->/c
;        (A10)
;        (->*
;         (g13 (->* () () (values A10)))
;         ()
;         (values A10)))
;   contract from: 
;       (interface for call-with-exception-handler)
;   blaming: (interface for call-with-exception-handler)
;    (assuming the contract is correct)
;   at: reproduction-write-file.rkt:3:3; original exception raised: create-content: asked to fail
; Context (errortrace):
;    reproduction-write-file.rkt:10:4: (error (quote create-content) "asked to fail")
;    reproduction-write-file.rkt:9:2: (when fail? (error (quote create-content) "asked to fail"))
;    /var/home/cadence/.racket/collects/racket/private/kw.rkt:1082:10: (define (create-content #:fail? (fail? #f)) (displayln "wa") (when fail? (error (quote ....) "asked to fail")) (displayln "finished writing"))
;    reproduction-write-file.rkt:18:3: (with-output-to-file #:exists (quote replace) file-name (λ () (create-content #:fail? ....)))
;    reproduction-write-file.rkt:13:0: (call-with-exception-handler (λ (e) (delete-file file-name) e) (λ () (with-output-to-file #:exists (quote ....) file-name ....)))
;    reproduction-write-file.rkt:13:0: (call-with-exception-handler (λ (e) (delete-file file-name) e) (λ () (with-output-to-file #:exists (quote ....) file-name ....)))

This error doesn't happen in regular Racket nor in Typed Racket without my proposed change. I have no idea what this error means, but I guess my proposal wasn't as good as I thought it was after all. I decided to switch to with-handlers and (raise e) and stop caring about it.

[mfelleisen]

Have you tried the following:

#lang typed/racket

(require/typed/provide racket/base
  [call-with-exception-handler (∀ (A) ((exn -> A) (-> A) -> A))])

(define file-name "test.txt")

(define (create-content #:fail? [fail? #f])
        (displayln "wa")
        (when fail?
          (error 'create-content "asked to fail"))
        (displayln "finished writing"))

(call-with-exception-handler
 (λ ({e : exn})
   (delete-file file-name)
   (raise e))
 (λ ()
   (with-output-to-file
       #:exists 'replace
     file-name
     (λ ()
       (create-content #:fail? #true)))))

I have two scripts that seem to resemble yours and I have run them since 1997 on a daily/monthly basis. Sam used them as part of his original typability evaluation.

[cloudrac3r]

(∀ (A) ((exn -> A) (-> A) -> A))

You didn't read the above discussion. This type is wrong. The exception handler return value is not like with-handlers. The first function does not return A. It returns something to raise. Only the second function returns A.

The only reason your code runs without a contract error is because your (raise e) in the first function means the first function never completes, so it never sees a contract error from checking what it returned.

---

A better approximation would be (∀ (A) ((exn -> exn) (-> A) -> A)), but this still isn't right because technically any value can be raised:

#lang typed/racket/base
(require/typed/provide racket/base
  [call-with-exception-handler (∀ (A) ((exn -> exn) (-> A) -> A))])

(call-with-exception-handler
 values
 (λ ()
   (raise "no")))

; exception raised by exception handler: call-with-exception-handler: broke its own contract
;   promised: exn?
;   produced: "no"

---

I messed around with it a bit more, and at some point I got the following error message:

Type Checker: Polymorphic function `call-with-exception-handler1' could not be applied to arguments:
; Argument 1:
;   Expected: (-> Any (U (Rec flat (U (Immutable-HashTable flat flat) (Immutable-Vectorof flat) (Pairof flat flat) Boolean Bytes Char Complex Keyword Null String Symbol)) exn))
;   Given:    (-> Any Any)
; Argument 2:
;   Expected: (-> A)
;   Given:    (-> Void)

The ridiculous type can be traced back to here in the code. Not sure how this relates to errors, but it has given me a type declaration that I haven't been able to break with code:

#lang typed/racket/base
(require/typed/provide racket/base
  [call-with-exception-handler (∀ (A) (((U (Rec flat (U (Immutable-HashTable flat flat) (Immutable-Vectorof flat) (Pairof flat flat) Boolean Bytes Char Complex Keyword Null String Symbol)) exn) -> (U (Rec flat (U (Immutable-HashTable flat flat) (Immutable-Vectorof flat) (Pairof flat flat) Boolean Bytes Char Complex Keyword Null String Symbol)) exn)) (-> A) -> A))])

;; <try anything here, I couldn't break it>

So feel free to use that one if you like it.