The Compiler's Handling of Types

The most unusual features of the SBCL compiler (which is very similar to the original CMU CL compiler, also known as Python) is its unusually sophisticated understanding of the Common Lisp type system and its unusually conservative approach to the implementation of type declarations. These two features reward the use of type declarations throughout development, even when high performance is not a concern. (Also, as discussed in the chapter on performance, the use of appropriate type declarations can be very important for performance as well.)

The SBCL compiler, like the related compiler in CMU CL, treats type declarations much differently than other Lisp compilers. By default (i.e., at ordinary levels of the safety compiler optimization parameter), the compiler doesn't blindly believe most type declarations; it considers them assertions about the program that should be checked.

The SBCL compiler also has a greater knowledge of the Common Lisp type system than other compilers. Support is incomplete only for the not, and and satisfies types.

Implementation Limitations

Ideally, the compiler would consider all type declarations to be assertions, so that adding type declarations to a program, no matter how incorrect they might be, would never cause undefined behavior. As of SBCL version 0.8.1, the compiler is known to fall short of this goal in two areas:

These are important bugs, but are not necessarily easy to fix, so they may, alas, remain in the system for a while.

Type Errors at Compile Time

If the compiler can prove at compile time that some portion of the program cannot be executed without a type error, then it will give a warning at compile time. It is possible that the offending code would never actually be executed at run-time due to some higher level consistency constraint unknown to the compiler, so a type warning doesn't always indicate an incorrect program. For example, consider this code fragment:

(defun raz (foo)
  (let ((x (case foo
             (:this 13)
             (:that 9)
             (:the-other 42))))
    (declare (fixnum x))
    (foo x)))
Compilation produces this warning:
in: DEFUN RAZ
  (CASE FOO (:THIS 13) (:THAT 9) (:THE-OTHER 42))
--> LET COND IF COND IF COND IF
==>
  (COND)
caught WARNING: This is not a FIXNUM:
  NIL
In this case, the warning means that if foo isn't any of :this, :that or :the-other, then x will be initialized to nil, which the fixnum declaration makes illegal. The warning will go away if ecase is used instead of case, or if :the-other is changed to t.

This sort of spurious type warning happens moderately often in the expansion of complex macros and in inline functions. In such cases, there may be dead code that is impossible to correctly execute. The compiler can't always prove this code is dead (could never be executed), so it compiles the erroneous code (which will always signal an error if it is executed) and gives a warning.

Type warnings are inhibited when the sb-ext:inhibit-warnings optimization quality is 3. (See the section on compiler policy.) This can be used in a local declaration to inhibit type warnings in a code fragment that has spurious warnings.

Precise Type Checking

With the default compilation policy, all type declarations are precisely checked, except in a few situations where they are simply ignored instead. Precise checking means that the check is done as though typep had been called with the exact type specifier that appeared in the declaration. In SBCL, adding type declarations makes code safer. (Except that as noted elsewhere, remaining bugs in the compiler's handling of types unfortunately provide some exceptions to this rule.)

If a variable is declared to be (integer 3 17) then its value must always be an integer between 3 and 17. If multiple type declarations apply to a single variable, then all the declarations must be correct; it is as though all the types were intersected producing a single and type specifier.

Argument and result type declarations are automatically enforced. If you declare the type of a function argument, a type check will be done when that function is called. In a function call, the called function does the argument type checking.

The types of structure slots are also checked. The value of a structure slot must always be of the type indicated in any :type slot option.

In traditional Common Lisp compilers, not all type assertions are checked, and type checks are not precise. Traditional compilers blindly trust explicit type declarations, but may check the argument type assertions for built-in functions. Type checking is not precise, since the argument type checks will be for the most general type legal for that argument. In many systems, type declarations suppress what little type checking is being done, so adding type declarations makes code unsafe. This is a problem since it discourages writing type declarations during initial coding. In addition to being more error prone, adding type declarations during tuning also loses all the benefits of debugging with checked type assertions.

To gain maximum benefit from the compiler's type checking, you should always declare the types of function arguments and structure slots as precisely as possible. This often involves the use of or, member, and other list-style type specifiers.

Weakened Type Checking

At one time, CMU CL supported another level of type checking, "weakened type checking", when the value for the speed optimization quality is greater than safety, and safety is not 0. The CMU CL manual still has a description of it, but even the CMU CL code no longer corresponds to the manual. Some of this partial safety checking lingers on in SBCL, but it's not a supported feature, and should not be relied on. If you ask the compiler to optimize speed to a higher level than safety, your program is performing without a safety net, because SBCL may at its option believe any or all type declarations with either partial or nonexistent runtime checking.

Getting Existing Programs to Run

Since SBCL's compiler, like CMU CL's compiler, does much more comprehensive type checking than most Lisp compilers, SBCL may detect type errors in programs that have been debugged using other compilers. These errors are mostly incorrect declarations, although compile-time type errors can find actual bugs if parts of the program have never been tested.

Some incorrect declarations can only be detected by run-time type checking. It is very important to initially compile a program with full type checks (high safety optimization) and then test this safe version. After the checking version has been tested, then you can consider weakening or eliminating type checks. This applies even to previously debugged programs, because the SBCL compiler does much more type inference than other Common Lisp compilers, so an incorrect declaration can do more damage.

The most common problem is with variables whose constant initial value doesn't match the type declaration. Incorrect constant initial values will always be flagged by a compile-time type error, and they are simple to fix once located. Consider this code fragment:

(prog (foo)
  (declare (fixnum foo))
  (setq foo ...)
  ...)
Here foo is given an initial value of nil, but is declared to be a fixnum. Even if it is never read, the initial value of a variable must match the declared type. There are two ways to fix this problem. Change the declaration
(prog (foo)
  (declare (type (or fixnum null) foo))
  (setq foo ...)
  ...)
or change the initial value
(prog ((foo 0))
  (declare (fixnum foo))
  (setq foo ...)
  ...)
It is generally preferable to change to a legal initial value rather than to weaken the declaration, but sometimes it is simpler to weaken the declaration than to try to make an initial value of the appropriate type.

Another declaration problem occasionally encountered is incorrect declarations on defmacro arguments. This can happen when a function is converted into a macro. Consider this macro:

(defmacro my-1+ (x)
  (declare (fixnum x))
  `(the fixnum (1+ ,x)))
Although legal and well-defined Common Lisp code, this meaning of this definition is almost certainly not what the writer intended. For example, this call is illegal:
(my-1+ (+ 4 5))
This call is illegal because the argument to the macro is (+ 4 5), which is a list, not a fixnum. Because of macro semantics, it is hardly ever useful to declare the types of macro arguments. If you really want to assert something about the type of the result of evaluating a macro argument, then put a the in the expansion:
(defmacro my-1+ (x)
  `(the fixnum (1+ (the fixnum ,x))))
In this case, it would be stylistically preferable to change this macro back to a function and declare it inline.

Some more subtle problems are caused by incorrect declarations that can't be detected at compile time. Consider this code:

(do ((pos 0 (position #\a string :start (1+ pos))))
    ((null pos))
  (declare (fixnum pos))
  ...)
Although pos is almost always a fixnum, it is nil at the end of the loop. If this example is compiled with full type checks (the default), then running it will signal a type error at the end of the loop. If compiled without type checks, the program will go into an infinite loop (or perhaps position will complain because (1+ nil) isn't a sensible start.) Why? Because if you compile without type checks, the compiler just quietly believes the type declaration. Since the compiler believes that pos is always a fixnum, it believes that pos is never nil, so (null pos) is never true, and the loop exit test is optimized away. Such errors are sometimes flagged by unreachable code notes, but it is still important to initially compile and test any system with full type checks, even if the system works fine when compiled using other compilers.

In this case, the fix is to weaken the type declaration to (or fixnum null). [1] Note that there is usually little performance penalty for weakening a declaration in this way. Any numeric operations in the body can still assume that the variable is a fixnum, since nil is not a legal numeric argument. Another possible fix would be to say:

(do ((pos 0 (position #\a string :start (1+ pos))))
    ((null pos))
  (let ((pos pos))
    (declare (fixnum pos))
    ...))
This would be preferable in some circumstances, since it would allow a non-standard representation to be used for the local pos variable in the loop body.

Notes

[1]

Actually, this declaration is unnecessary in SBCL, since it already knows that position returns a non-negative fixnum or nil.