On 29 December 2011 12:24, Juan Jose Garcia-Ripoll juanjose.garciaripoll@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