[R6RS] Safe/unsafe mode

[William D Clinger]

Kent wrote:
> Here's a revised safety proposal, with answers to Will's questions.

Thank you!  By my count, we now have three reasonably
coherent proposals on the table.  None of the three are
described by the current draft of draft/safety/safety.txt,
so I will revise that file to present all three, inserting
bracketed FIXME remarks where I believe some further
clarifications or improvements are necessary.

> 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.)

> Must the following code
> raise an exception, assuming there are no declarations other than
> the ones shown?
> 
>   (define (f)
>     (declare unsafe)
>     (let ([g (lambda (x)
>                (declare safe)
>                (car x))])
>       g))
> 
>   (let ([g (f)]) (g 'a))

Yes, this too must raise an exception under the
semantics I prefer.

> 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?

> 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?

> (\#primitive n prim) can be abbreviated #n%prim.  A primitive reference
> resulting from a reference to an import from the scheme (or r5rs,
> etc.) module is expanded into #2%prim by default, except in optimize-level
> 3 (unsafe) code, where it is expanded into #3%prim.  The \#primitive or
> #n%prim syntax can also be used directly in source code.
> 
> The optimizer propagates the entire \#primitive form, not just the
> primitive name, as the following transcript shows.
[....]
> The only thing presently missing in Chez Scheme is a way to locally mark a
> subexpression of a top-level expression (larger than an identifier) safe
> or unsafe.  Instead, the entire top-level expression is treated as safe or
> unsafe, except for primitives explicitly marked with #2% or #3%, depending
> on the value of the optimize-level parameter.

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.

> It is not sensitive to the name by which a procedure is called, but rather
> to whether the value is a safe or unsafe version of the primitive.

But whether you get the safe or unsafe value depends upon
whether you used the safe or unsafe binding.  The critical
part of your semantics has to do with how those bindings
are introduced.  It still looks to me as though you expect
those bindings to be introduced non-hygienically, at the
declaration points.

Will