5.3.6 Type Check Optimization

     

Python backs up its support for precise type checking by minimizing the cost of run-time type checking. This is done both through type inference and though optimizations of type checking itself.

Type inference often allows the compiler to prove that a value is of the correct type, and thus no type check is necessary. For example:

(defstruct foo a b c)
(defstruct link
  (foo (required-argument) :type foo)
  (next nil :type (or link null)))

(foo-a (link-foo x))

Here, there is no need to check that the result of link-foo is a foo, since it always is. Even when some type checks are necessary, type inference can often reduce the number:

(defun test (x)
  (let ((a (foo-a x))
        (b (foo-b x))
        (c (foo-c x)))
    ...))

In this example, only one (foo-p x) check is needed. This applies to a lesser degree in list operations, such as:

(if (eql (car x) 3) (cdr x) y)

Here, we only have to check that x is a list once.

Since Python recognizes explicit type tests, code that explicitly protects itself against type errors has little introduced overhead due to implicit type checking. For example, this loop compiles with no implicit checks checks for car and cdr:

(defun memq (e l)
  (do ((current l (cdr current)))
      ((atom current) nil)
    (when (eq (car current) e) (return current))))

  Python reduces the cost of checks that must be done through an optimization called complementing. A complemented check for type is simply a check that the value is not of the type (not type). This is only interesting when something is known about the actual type, in which case we can test for the complement of (and known-type (not type)), or the difference between the known type and the assertion. An example:

(link-foo (link-next x))

Here, we change the type check for link-foo from a test for foo to a test for:

(not (and (or foo null) (not foo)))

or more simply (not null). This is probably the most important use of complementing, since the situation is fairly common, and a null test is much cheaper than a structure type test.

Here is a more complicated example that illustrates the combination of complementing with dynamic type inference:

(defun find-a (a x)
  (declare (type (or link null) x))
  (do ((current x (link-next current)))
      ((null current) nil)
    (let ((foo (link-foo current)))
      (when (eq (foo-a foo) a) (return foo)))))

This loop can be compiled with no type checks. The link test for link-foo and link-next is complemented to (not null), and then deleted because of the explicit null test. As before, no check is necessary for foo-a, since the link-foo is always a foo. This sort of situation shows how precise type checking combined with precise declarations can actually result in reduced type checking.