Bug with letrec call/cc interaction

[pylasnier]

If a lambda re-enters a letrec initialisation expression using a continuation from call/cc, and specifically that lambda is referred to in both branches of an if-expression, it will have the wrong behaviour.

For background, letrec differs from letrec*, in that letrec assigns all of its variables after all of their corresponding initialisation expressions have been evaluated, whereas letrec* assigns its variables one at a time after each corresponding initialisation expression has been evaluated. This difference leads to different behaviours with the following program, which mutates one of the letrec variables before re-entering another variable by its contiuation:

(let ((f (lambda ()
                 (letrec[*] ((a 4) (j (call/cc (lambda (cc) cc))))
                     (if (eqv? j 0)
                         a
                         (begin
                          (set! a 9)
                          (j 0)))))))
      (f))

With letrec* the mutation persists and results in the value 9, because a has already been initialised by the point of the call/cc. With letrec, the mutation is overwritten back to a 4, because a has not yet been initialised by the point of the call/cc, and is assigned 4 again after re-entering the initialisation expression for j.

Chez Scheme has the correct behaviour in this example. However, if f is instead reached through an if-expression, and particularly if f is referenced in both branches, letrec has the incorrect behaviour which seems to correspond with letrec*, and gives 9 rather than 4.

(let ((f (lambda ()
                 (letrec ((a 4) (j (call/cc (lambda (cc) cc))))
                     (if (eqv? j 0)
                         a
                         (begin
                          (set! a 9)
                          (j 0)))))))
      (if #t (f) (f)))

This example incorrectly produces 9. The correct behaviour should be to produce 4. This happens regardless if the true or false branch is taken. It does not happen if f is only referred to in one of the branches, i.e. (if #t (f) 0) gives 4.

Tested on 10.2.0, NixOS. Correct behaviour witnessed on Chicken.

[gwatt]

The order of evaluation of the binding form expressions in letrec is unspecified. I think it's wrong to assume either behavior is correct. Definitely a little odd that changing (f) to (if #t (f) (f)) changes the behavior though.

[pylasnier]

Order of evaluation is not relevant here, because what matters is that assignment to variables a and j occurs after evaluating their initialisation expressions for letrec, regardless of the order those were evaluated in. a should always be reassigned 4, hence the behaviour with the if-expression is incorrect.

[mflatt]

I think the issue here is that the right-hand side of a letrec[*] binding is not supposed to return multiple times per R6RS and TSPL.

[pylasnier]

Chez Scheme is R6RS, where the behaviour for returning an initialisation expression is underspecified. It is importantly, however, not unspecified: there are only two valid behaviours, which is to raise an exception or re-return the expression anyway (section A.11 in R6RS spec).

Chez Scheme is not opting to raise an exception in this example, hence it must follow the second possible behaviour which is to return the expression. The semantics in this case would dictate the function returns 4. Clearly Chez Scheme is doing this, because it does usually return 4, just not in this edge case where f shows up twice.

Just to be sure, I have also tested this example with Racket using R6RS. Racket also has the correct behaviour. It's only Chez Scheme which has this behaviour, and only for this edge case. This is a semantic bug.

[mflatt]

My read of R6RS "Implementations may or may not detect that the continuation of each is invoked more than once" is not that it requires a certain behavior when not detecting multiple invocations. I would concede that the standard isn't clear, at best, and I may still be misreading. But I think the interpretation of the standard as having undefined behavior on this point is fairly deeply ingrained in Chez Scheme passes in the vicinity of cp0, in which case it would be no small matter to change the interpretation.

Racket generally promises specific behavior where RnRS leaves things unspecified. That reflects my opinion on what an implementation should do, but not my opinion of what the standard says. :) Although Racket compiles to Chez Scheme, Racket pins down the semantics of letrec by performing its own expansion into let plus set! when a variable might be referenced too early or when a right-hand might return multiple times.

[pylasnier]

I agree that the informal semantics described in R6RS is somewhat ambiguous, but the formal semantics (in the appendix of the report) is not. The formal operational semantics captures these two possible behaviours by keeping track of a flag which is set after the first return. There are then two rules for returning an initialisation expression when the flag is already set: one rule raises an exception, the other rule ignores the flag and proceeds as normal. It is worth noting here that the report describes these two rules as being "in keeping with the two legal behaviors of letrec and letrec*". There are two legal behaviours, without ambiguity, and the behaviour from this issue is not one of them. With this in mind, I would interpret the informal semantic description of the report to mean that an implementation may not 'detect' an invocation of the initialisation expression, but that does not permit it to thereby have undefined behaviour. If this is indeed how Chez Scheme interprets the semantics, I think that is incorrect.

You will know more about the inner workings of Chez than me, but I am willing to bet that Chez Scheme does in fact follow the legal behaviour described in the report, because it does have the correct behaviour for this function (result 4), most of the time. It is just once f is duplicated, such as with an if-expression like this, that it no longer does. Again, Chicken and Racket both have the correct behaviour, including in this edge case where Chez changes behaviour.

I appreciate that this may, as you described, be a deeply ingrained behaviour, but I believe with great confidence that it is a bug. I'm also optimistic that fixing it should be feasible, because, as I have said, Chez has the correct behaviour for this funny function, most of the time.

[dybvig]

We opted for the weaker should not vs must not here and in other places when we felt that detecting incorrect behavior might be unduly complicated, inefficient, or both. The behavior of any program that does something it should not do is unspecified. Since an init should not return more than once, the behavior is unspecified when one does, and the current behavior in Chez Scheme is as valid as any other behavior.

That said, reliably detecting multiple returns from an init would be desirable if doing so adds no overhead for programs that adhere to the restriction. So if someone wants to take that on, I would be happy to see it.

The formal semantics is non-normative; it describes one way (actually, multiple ways) of implementing a portion of R6RS correctly rather than the only way(s).

[pylasnier]

I see, perhaps I have misunderstood the purpose of the formal semantics. I appreciate the clarification.

If raising an exception is currently not possible to implement effectively, would it still be a concern that the behaviour of this function changes depending on how it is used elsewhere? That doesn't sit well with me personally.