[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

safe/unsafe mode

This page is part of the web mail archives of SRFI 77 from before July 7th, 2015. The new archives for SRFI 77 contain all messages, not just those from before July 7th, 2015.

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.

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