Next: Source Optimization
Up: Type Inference
Previous: Dynamic Type Inference
  Contents
  Index
Type Check Optimization
optimization
type check
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))))
complemented type checks
Python reduces the cost of checks that must be done through an
optimization called complementing. A complemented check fortype 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 forfoo 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 explicitnull 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.
Next: Source Optimization
Up: Type Inference
Previous: Dynamic Type Inference
  Contents
  Index
Peter Van Eynde
2001-03-08