[pro] [imp-hackers] Declarations in compilers (feedback welcome)

[Nikodemus Siivola]

On 29 December 2011 12:24, Juan Jose Garcia-Ripoll
<juanjose.garciaripoll at googlemail.com> wrote:

> [b]- SBCL takes declarations (and THE) as type assertions. For instance, in
> (LET ((Y (FOO X))) (DECLARE (FIXNUM Y))) ...) the assignment to Y would be
> checked to be a FIXNUM. This means the type declaration is actually enforced
> and believed and only at SAFETY 0 the checks are dropped (*)

This is correct, but incomplete. At SAFETY 1 SBCL will weaken complex
assertions: eg.

  (OR (INTEGER 0 2) (INTEGER 7 10))

will be simplified to a range check for (INTEGER 0 10). At SAFETY 2 no
types are weakened. At SAFETY 3 all the extra bells and whistles
required by ANSI come into play.

CMUCL's approach is very similar to SBCL's, but IIRC the policy on
weakening assertions is a bit different.

> In both cases one ends up with a model in which in order to truly believe a
> declaration and have no extra burden (assertions), one has to drop to SAFETY
> 0 in all code that is involved with it, which is a mess, because it might
> inadvertently affect other parts of the code. It is for this reason that I
> am considering an alternative model for ECL which would grade safety as
> follows

Actual cost of assertions (for SBCL generated code at least) is fairly
small. They should for the most part be branches which the static
branch prediction model gets right every time.

> - Type declarations are always believed
> - SAFETY >= 1 adds type checks to enforce them.
> - SAFETY = 0, no checks.
> - SAFETY = 1, the special form THE or additional proclamations on the
> functions can be used to deactivate the check. As in (LET ((Y (THE FIXNUM
> (FOO X))) ...)
>
> This would allow one to keep most code safe, while deactivating some checks
> when they are really known to be true (**). Do you think this is
> useful/useless? The problem I see with this approach is that all code around
> is written for model [a] or [b], but I could not come up with something more
> sensible so far.

I somewhat dislike making THE a loophole -- IMO it complicates the
mental model necessary to understand how things work, especially if it
works differently at a specific SAFETY level. SBCL has
SB-EXT:TRULY-THE for just this purpose, which is roughly equivalent
to:

  (defmacro truly-the (type values)
    `(flet ((the-values () ,values))
       (declare (optimize (safety 0)))
       (the ,type (the-values))))

CMUCL has the equivalent as EXT:TRULY-THE. You may want to consider
something like that as well.

I know that when I write (UNSAFE-FUN-THAT-CHECKS-NOTHING (THE FIXNUM
X)) I intend the THE as an assertion. Granted, most of the code I
write is intended for SBCL-only consumption, so this is probably a
moot point. Still, loading bunch of stuff from Quicklisp and
instrumenting the compiler to see how often THE's like that occur
might be instructive.

At the end, as long as SAFETY 0 = trust everything blindly and SAFETY
3 = check everything, I think you're well within the bounds of custom
and sanity if you choose to make SAFETY 1 a bit magical.

> (*) Actually the checks are also deactivated when SBCL can infer the type of
> the value that is assigned to Y.

This is actually a major point for us. Because SBCL open codes /
partial-evaluates things rather agressively, and has a fairly
extensive derivation machinery, in idiomatic Lisp code with type
declarations type checks mostly occur only for function arguments,
return values, and iteration variables -- and the cost of those type
checks if trivial for the most part. What sometimes makes them look
more expensive then they actually are is the suboptimal representation
selection they cause.

> This is somewhat contradictory, because (SETF Y (THE FIXNUM (FOO X))) would still
> generate a check, but proclaiming FOO to return a FIXNUM would completely bypass
> the check.

Yes, but if you proclaim FOO to return a fixnum before compiling it,
then FOO will take care of that assertion. (Trusting proclamations
made after a function has been compiled is considered a long-standing
bug, not a feature.)

Cheers,

 -- Nikodemus