safe/unsafe mode

[Sebastian Egner <sebastian.egner@xxxxxxxxxxx>]

In general, I am very happy with this
SRFI because it is a
great improvement over R5RS. However,
I would like to
raise the following issue:

I think a global mode controlling
the behavior of the
arithmetic operations is a fundamentally
bad idea.

This approach was used in PASCAL, and
it did not work
as well in practice as it was hoped
for because the
proof obligation raised by switching
to 'unsafe mode' is 
"the entire program is arithmetically
correct," which can
occasionally be challenging to actually
prove.

Experience has shown that it is preferable
to have a
separate set of unsafe operations to
be used locally
when the programmer fully understands
the context in
which the operations are used, i.e.
when the associated
proof obligations are trivial---and
retain an 'oops detector'
in all other cases (of course the proof
obligations don't
go away when overflow will raises an
exception.)

Example: SRFI 42 (eager comprehensions)
contains the
generator :RANGE running through a sequence
of integers.
Currently, :RANGE is implemented using
the generic arithmetics
(there is no other in R5RS) but of course
99% of all loops
fit comfortably in the fixnum range
(in case it covers {0..2^30-1}.)
Ideally, :RANGE would produce code for
a fixnum loop with
unsafe operations, and resort to a bignum
loop if it detects
that this is necessary during loop initialization.
This is not entirely
straight-forward to do, because the
code for the body of the
loop must not be duplicated. Nevertheless,
it sounds feasible
(Compiler experts: is that so?) In effect,
:RANGE can use the
most efficient fixnum ops without any
leakage of proof obligation
from the SRFI 42 library into the application
program.

With a global mode switch, on the other
hand, the loop 
generated by :RANGE is less efficient
in 'safe' mode---and
after switching to 'unsafe' mode it
either *is* unsafe, or a
proof obligation ("loop range fits
into fixnum...") leaks out with
force ("...or all bets are off.")
Either way, the added value of
the mode switch is unclear: If I have
a proof obligation to use
FIXNUM properly in the anyhow, then
what is the point of 
'safe mode' in the first place?

Concerning other alternatives, e.g.
o Special forms (unsafe-arithmetics
<_expression_>) and
   (safe-arithmetics <_expression_>)
or
o Procedures (with-unsafe-arithmetics
<thunk>) etc.
it is not so clear what the impact will
be in practice. This could
easily mess up programs, and the mixture
with macros might
also be pretty explosive (think of using
unsafe-arithmetics 
around the *body* of a :RANGE macro
by accident; good
luck for hunting down the cuprit).


Reaching beyond the 'global mode' issue,
I would like to 
emphasize the following point of view.
As a designer for an 
arithmetic model you should ask yourself:

      Which information
determines the result of an arithmetic operation?

In R5RS:
1. The numerical value of the argument
objects.
2. The numerical type of the argument
objects.
3. The exactness/inexactness flag of
the argument objects.

In the current proposal for R6RS according
to SRFI 77 it is all of
the above plus:
4. The global safe/unsafe mode flag.

All these properties are dynamic properties
of the program, and
static analysis has a hard time in discovering
any of them, even
partially. The point Mike and I argued
in the 2004 Scheme Workshop
paper was that we would like to turn
3., and 4. into static properties
for polymorphic arithmetics and 2.,
3., and 4. for monomorphics.

Sebastian.
----
Dr. Sebastian Egner
Senior Scientist
Philips Research Laboratories
Prof. Holstlaan 4 (WDC 1-051, 1st floor, room 51)
5656 AA Eindhoven
The Netherlands
tel:       +31 40 27-43166
fax:      +31 40 27-44004
email: sebastian.egner@xxxxxxxxxxx