[R6RS] Safe/unsafe mode

[dyb at cs.indiana.edu]

> > As I understand your semantics, all bets are off if safe code nested
> > within unsafe code is run from the unsafe code, so that:
> > 
> >   (define (f)
> >     (declare unsafe)
> >     (let ([g (lambda (x)
> >                (declare safe)
> >                (car x))])
> >       (g 'a)))
> > 
> > does not necessarily raise an exception.
>
> No, I believe the code above must raise an exception
> under the semantics I prefer.  The procedure g has no
> documented constraints on its argument (indeed, it is
> impossible to express such constraints in R6RS Scheme
> as I expect it to be), so calling g with the symbol a
> is perfectly all right.  The procedure g then calls
> car on that symbol, but does so from safe code, so the
> car procedure must raise an exception.  (In terms of
> the operational model, g calls car through its safe
> entry point.)

Thanks for your patience in answering my questions.  Unfortunately, this
confuses me further.  Based on your proposal and earlier examples, I was
pretty sure you would say that an exception did not have to be raised. 
Your proposal says:

  If unsafe code does something that might generate an exception or cause
  unspecified behavior, then all bets are off.

Calling g with a symbol definitely "does something" that raises an
exception, so all bets should be off.  Can you offer up something more
precise than "does something" to justify why all bets are not off in this
case?

Based on your response, I'm guessing that

  (let ((f (lambda (x) (- x))))
    (declare unsafe)
    (f '(a)))

must raise an exception, so a compiler cannot eta reduce (lambda (x) (- x))
to - and propagate -, nor inline the body of f at its call site, either
of which would produce:

  (let ()
    (declare unsafe)
    (- '(a)))

Right?

You say that g has no documented constraints.  Is there a way to document
constraints of user-defined procedures?  If not, are the safe and unsafe
entry points of each user-defined procedure always the same?

> > I'm not sure this model explains everything, but never mind that.  The
> > correspondingly simple model for my semantics is that each identifier
> > exported from a standard library has two bindings, a safe one referenced
> > from safe code and an unsafe one referenced from unsafe code.  Of course,
> > the unsafe one may behave exactly the same as the unsafe one.
>
> Okay.  That was pretty much the model I expected: two
> possible bindings for each identifier in a standard
> library.  It appears to me that your model treats the
> standard libraries specially, so only the identifiers
> mentioned in R6RS will have these two possible bindings.
> Correct?

Correct.  Implementations (and R7RS) may extend the model further, and
library and application developers can create unsafe versions of their own
operators by whatever mechanism they please.  The only thing we need to
provide for them, if they're going to have it, is unsafe versions of the
built-in operators.  This appears to be all your model provides, too,
although it's possible I still don't understand your model.

> > In the output of the expander, Chez Scheme identifies each primitive
> > reference as safe or unsafe using the syntax (\#primitive n prim),
> > where for historical reasons, n=2 for safe and n=3 for unsafe.
>
> I assume this applies only to identifiers mentioned in
> the R5RS.  If it applies to identifiers not mentioned
> in the R5RS, how does a programmer express his/her
> intentions with respect to the unsafe binding?

It applies more generally to identifiers bound in the scheme module,
i.e., all that are defined by Chez Scheme, of which the ones mentioned
in R5RS are a subset.

> And, of course, you think it would be good for all other
> implementors to have to change their compilers to coincide
> with the semantics of Chez Scheme.

I would like other implementations to implement the safety semantics I
have proposed, or I wouldn't have proposed it.  The fact that a model is
implemented by some existing compiler should be a point in its favor,
since it serves to verify that the model can actually be implemented.

I don't care how or if other implementations perform copy propagation.  I
showed how Chez Scheme does it only to offer proof that copy propagation
can be done with my model, to counter your implication to the contrary.

Kent