Previous: Dynamic Type Inference, Up: Type Inference [Contents][Index]
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.
Previous: Dynamic Type Inference, Up: Type Inference [Contents][Index]