@comment{ -*- Dictionary: papers -*-}
@make[report]
@Use(Database "/afs/cs/project/clisp/scribe/database/")
@Libraryfile[Uttir]
@String(IndexFuns "Yes")
@commandstring(dash = "@Y[M]")
@commandstring[alien = "Alien"]
@commandstring[aliens = "Aliens"]
@commandstring[hemlock = "Hemlock"]
@commandstring[python = "Python"]
@commandstring[cmucl = "CMU Common Lisp"]
@commandstring[llisp = "Common Lisp"]
@commandstring[cltl = "@i[Common Lisp: The Language]"]


@begin[comment]

Some information on how type inference is done:
    bottom-up static
    dynamic
    inter-routine

Need more context, references, implications, conclusions.

Have I really conveyed the "feel" of precise type checking?

Anecdotal summary of the effects:
    precise type checking
    compile time type errors
    dead code notes

Numbers on overhead of type checking:
    full
    weak
    none
    conventional (delta of allegro fast v.s. safe?)

Overview of the importance of safety for productivity.
    Need refs for safety, assertions?
    Describe the usefulness of complex types for describing data-structure
    invariants.  This eliminates many problems with data structures becoming
    inconsistent but the inconsistency only being discovered later on.

Overview of the importance of type information for efficiency.
    Should have some material on number representations.

Eliminate uses of "you"
"In Python"?
"The compiler" v.s. "Python"

reference current practice.  Look for "traditional", "conventional" and "other"
compilers.

@end[comment]

@section[Types in Python]

A big difference between @Python and all other @llisp compilers is the approach
to type checking and amount of knowledge about types:
@begin[itemize]
@Python treats type declarations much differently that other Lisp compilers do.
@Python doesn't blindly believe type declarations; it considers them assertions
about the program that should be checked.

@Python also has a tremendously greater knowledge of the @clisp type system
than other compilers.
@end[itemize]

This is a win because:
@begin[itemize]
Precise type checking helps to find bugs at run time.

Compile-time type checking helps to find bugs at compile time.

Type inference minimizes the need for generic operations, and also increases
the efficiency of run time type checking and the effectiveness of compile time
type checking.

Support for detailed types provides a wealth of opportunity for 
operation-specific type inference and optimization.
@end[itemize]


@section[Compile Time Type Errors]

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:
@lisp
(defun raz (foo)
  (let ((x (case foo
	     (:this 13)
	     (:that 9)
	     (:the-other 42))))
    (declare (fixnum x))
    (foo x)))
@endlisp
Compilation produces this warning:
@lisp
In: DEFUN RAZ
  (CASE FOO (:THIS 13) (:THAT 9) (:THE-OTHER 42))
--> LET COND IF COND IF COND IF 
==>
  (COND)
Warning: This is not a FIXNUM:
  NIL
@endlisp
In this case, the warning is telling you that if @f[foo] isn't any of
@f[:this], @f[:that] or @f[:the-other], then @f[x] will be initialized to
@false, which the @f[fixnum] declaration makes illegal.  The warning will go
away if @f[ecase] is used instead of @f[case], or if @f[:the-other] is changed
to @true.

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.



@section[Precise Type Checking]
@label[precise-type-checks]

With the default compilation policy, all type assertions are precisely
checked.  Precise checking means that the check is done as though @f[typep] had
been called with the exact type specifier that appeared in the declaration.
@Python uses the @i[policy] specified by the @f[optimize] declaration to
determine whether to trust type assertions.  Type assertions from declarations
are indistinguishable from the type assertions on arguments to built-in
functions.  In @Python, adding type declarations makes code safer.

If a variable is declared to be @w<@f<(integer 3 17)>>, then its value must
always always be an integer between @f[3] and @f[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
@f[and] type specifier.

Argument 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, which
means that a more restrictive type assertion in the calling function (e.g.,
from @f[the]) may be lost.

The types of structure slots are also checked.  The value of a structure slot
must always be of the type indicated in any @f[:type] slot option.  Because of
precise argument type checking, the arguments to slot accessors are checked to
be the correct type of structure.

@b[### reference current practice...]

In traditional @llisp 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 @Python'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 @f[or], @f[member] and other list-style type
specifiers.  Paradoxically, even though adding type declarations introduces
type checks, it usually reduces the overall amount of type checking.  This is
especially true for structure slot type declarations.

@Python uses the @f[safety] optimization quality (rather than presence or
absence of declarations) to choose one of three levels of run-time type error
checking.


@section[Weakened Type Checking]
@label[weakened-type-checks]

When the value for the @f[speed] optimization quality is greater than
@f[safety], and @f[safety] is not @f[0], then type checking is weakened to
reduce the speed and space penalty.  In structure-intensive code this can
double the speed, yet still catch most type errors.  Weakened type checks
provide a level of safety similar to that of "safe" code in other @llisp
compilers.

A type check is weakened by changing the check to be for some convenient
supertype of the asserted type.  For example, @f<@w<(integer 3 17)>> is changed
to @f[fixnum], @f<@w<(simple-vector 17)>> to @f[simple-vector], and structure
types are changed to @f[structure].  A complex check like:
@lisp
(or node hunk (member :foo :bar :baz))
@endlisp
will be omitted entirely (i.e., the check is weakened to @f[*].)  If a precise
check can be done for no extra cost, then no weakening is done.

Although weakened type checking is similar to type checking done by other
compilers, it is sometimes safer and sometimes less safe.  Weakened checks are
done in the same places as precise checks, so all the preceding discussion
about where checking is done still applies.  Weakened checking is sometimes
somewhat unsafe because although the check is weakened, the precise type is
still input into type inference.  In some contexts this will result in type
inferences not justified by the weakened check, and hence deletion of some type
checks that would be done by conventional compilers.

For example, if this code was compiled with weakened checks:
@lisp
(defstruct foo
  (a nil :type simple-string))

(defstruct bar
  (a nil :type single-float))

(defun myfun (x)
  (declare (type bar x))
  (* (bar-a x) 3.0))
@endlisp
and @f[myfun] was passed a @f[foo], then no type error would be signalled, and
we would try to multiply a @f[simple-vector] as though it were a float (with
unpredictable results.)  This is because the check for @f[bar] was weakened to
@f[structure], yet when compiling the call to @f[bar-a], the compiler thinks it
knows it has a @f[bar].


@section[Getting Existing Programs to Run]

Since @Python does much more comprehensive type checking than other Lisp
compilers, @Python will detect type errors in many 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 important to initially compile programs with full type checks and then test
this version.  @Python does much more type inference than other @llisp
compilers, so believing an incorrect declaration does much more damage.

The most common problem is with variables whose initial value doesn't match the
type declaration.  Incorrect initial values will always be flagged by a
compile-time type error, and they are simple to fix once located.  Consider
this code fragment:
@lisp
(prog (foo)
  (declare (fixnum foo))
  (setq foo ...)
  ...)
@endlisp
Here the variable @f[foo] is given an initial value of @false, but is declared
to be a @f[fixnum].  Even if it is never read, the initial value of a variable
must match the declared type.  This code can be made correct either by changing
the declaration to @w<@f<(or fixnum null)>> or changing the initial value to
@f[0].

Some more subtle problems are caused by incorrect declarations that can't be
detected at compile time.  Consider this code:
@lisp
(do ((pos 0 (position #\a string :start (1+ pos))))
    ((null pos))
  (declare (fixnum pos))
  ...)
@endlisp
Although @f[pos] is almost always a @f[fixnum], it is @false 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
@f[position] will complain because @w<@f[(1+ nil)]> isn't a sensible start.)
Why?  Because if you compile without type checks, the compiler just quietly
believes the type declaration.  Since @f[pos] is always a @f[fixnum], it is
never @nil, so @w<@f[(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 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
@w<@f[(or fixnum null)]>.  Note that there is usually little
performance penalty for weakening a declaration in this way.  Any numeric
operations in the body can still assume the variable is a @f[fixnum], since
@false is not a legal numeric argument.


@section[More Types Meaningful]

@clisp has a very powerful type system, but conventional @llisp implementations
typically only recognize the small set of types special in that
implementation.  In these systems, there is an unfortunate paradox: a
declaration for a relatively general type like @f[fixnum] will be recognized by
the compiler, but a highly specific declaration such as @f[@w<(integer 3 17)>]
is totally ignored.

@b[### reference current practice]

This is obviously a problem, since the user has to know how to specify the type
of an object in the way the compiler wants it.  A very minimal (but rarely
satisfied) criterion for type system support is that it be no worse to make a
specific declaration than to make a general one.  @python goes beyond this by
exploiting a number of advantages obtained from detailed type information.

Using more restrictive types in declarations allows the compiler to do better
type inference and more compile-time type checking.  Also, when type
declarations are considered to be consistency assertions that should be
verified (conditional on policy), then complex types are useful for making more
detailed assertions.

Python "understands" the list-style @f[or], @f[member], @f[function], array and
number type specifiers.  Understanding means that:
@begin[itemize]
If the type contains more information than is used in a particular context,
then the extra information is simply ignored, rather than derailing type
inference.

In many contexts, the extra information from these type specifier is used to
good effect.  In particular, type checking in @f[Python] is @i[precise], so
these complex types can be used in declarations to make interesting assertions
about functions and data structures.  More specific declarations also aid type
inference and reduce the cost for type checking.
@end[itemize]


@section[Canonicalization]

When given a type specifier, @python will often rewrite it into a different
(but equivalent) type.  This is the mechanism that @python uses for detecting
type equivalence.  For example, in @python's canonical representation, these
types are equivalent:
@lisp
(or list (member :end)) <==> (or cons (member nil :end))
@endlisp
The main significance of this canonicalization is that all semantically
equivalent type specifiers really are considered equivalent by the compiler.
The standard symbol type specifiers for @f[atom], @f[null], @f[fixnum], etc.,
are in no way magical.  The @f[null] type is actually defined to be
@f<@w<(member nil)>>, @f[list] is @f<@w<(or cons null)>>, and @f[fixnum] is 
@f<@w<(signed-byte 30)>>.  

@section[Structure Types]
@label[structure-types]

@b[### reference current practice]

Because of precise type checking, structure types are much better supported by
Python than by conventional compilers:
@begin[itemize]
The structure argument to structure accessors is precisely checked @dash if you
call @f[foo-a] on a @f[bar], an error will be signalled.

The types of slot values are precisely checked @dash if you pass the wrong type
argument to a constructor or a slot setter, then an error will be signalled.
@end[itemize]
This error checking is tremendously useful for detecting bugs in programs that
manipulate complex data structures.

An additional advantage of checking structure types and enforcing slot types
is that the compiler can safely believe slot type declarations.  @python
effectively moves the type checking from the slot access to the slot setter or
constructor call.  This is more efficient since caller of the setter or
constructor often knows the type of the value, entirely eliminating the need to
check the value's type.  Consider this example:
@lisp
(defstruct coordinate
  (x nil :type single-float)
  (y nil :type single-float))

(defun make-it ()
  (make-coordinate 1.0 1.0))

(defun use-it (it)
  (declare (type coordinate it))
  (sqrt (expt (coordinate-x it) 2) (expt (coordinate-y it) 2)))
@endlisp
@f[make-it] and @f[use-it] are compiled with no checking on the types of the
float slots, yet @f[use-it] can use @f[single-float] arithmetic with perfect
safety.  Note that @f[make-coordinate] must still check the values of @f[x] and
@f[y] unless the call is block compiled or inline expanded.  But even without
this advantage, it is almost always more efficient to check slot values on
structure initialization, since slots are usually written once and read many
times.

@section[Type Restrictions]

Avoid use of the @f[and], @f[not] and @f[satisfies] types in declarations,
since type inference has problems with them.  When these types do appear in a
declaration, they are still checked precisely, but the type information is of
limited use to the compiler.  @f[and] types are effective as long as the
intersection can be canonicalized to a type that doesn't use @f[and].  For
example:
@lisp
(and fixnum unsigned-byte)
@endlisp
is fine, since it is the same as:
@lisp
(integer 0 @i[most-positive-fixnum])
@endlisp
but this type:
@lisp
(and symbol (not (member :end)))
@endlisp
will not be fully understood by type interference since the @f[and] can't be
removed by canonicalization.

Using any of these type specifiers in a type test with @f[typep] or
@f[typecase] is fine, since as tests, these types can be translated into the
@f[and] macro, the @f[not] function or a call to the satisfies predicate.

@section[Style Recommendations]

@b[### Flush this section???]

Python provides good support for some currently unconventional ways of using
the @clisp type system.  With @python, it is desirable to make declarations as
precise as possible, but type inference also makes some declarations
unnecessary.  Here are some general guidelines for maximum robustness and
efficiency:
@begin[itemize]
Declare the types of all function arguments and structure slots as precisely as
possible (while avoiding @f[not], @f[and] and @f[satisfies]).  Put in these
declarations during initial coding so that type assertions can find bugs for
you during debugging.

Use the @f[member] type specifier where there are a small number of possible
symbol values, for example: @w<@f<(member :red :blue :green)>>.

Use the @f[or] type specifier in situations where the type is not certain, but
there are only a few possibilities, for example:
@w<@f<(or list vector)>>.

Declare integer types with the tightest bounds that you can, such as 
@f<@w<(integer 3 7)>>.

In addition to declaring the array element type and simpleness, also declare
the dimensions if they are fixed, for example:
@lisp
(simple-array single-float (1024 1024))
@endlisp
This bounds information allows array indexing for multi-dimensional arrays to
be compiled much more efficiently, and may also allow array bounds checking to
be done at compile time.

Avoid use of the @f[the] declaration within expressions.  Not only does it
clutter the code, but it is also almost worthless under safe policies.  If the
need for an output type assertion is revealed by efficiency notes during
tuning, then you can consider @f[the], but it is preferable to constrain the
argument types more, allowing the compiler to prove the desired result type.

Don't bother declaring the type of @f[let] or other non-argument variables
unless the type is non-obvious.  If you declare function return types and
structure slot types, then the type of a variable is often obvious both to the
programmer and to the compiler.  An important case where the type isn't
obvious, and a declaration is appropriate, is when the value for a variable is
pulled out of untyped structure (e.g., the result of @f[car]), or comes from
some weakly typed function, such as @f[read].
@end[itemize]


@section[Type Inference]
@label[type-inference]

Type inference is the process by which the compiler tries to figure out the
types of expressions and variables, given an inevitable lack of complete type
information.  Although @python does much more type inference than most @llisp
compilers, remember that the more precise and comprehensive type declarations
are, the more type inference will be able to discover.

@section[Variable Type Inference]
@label[variable-type-inference]

The type of a variable is the union of the types of all the definitions.  In
the degenerate case of a let, the type of the variable is the type of the
initial value.  This inferred type is intersected with any declared type, and
is then propagated to all the variable's references.  The types of
@f[multiple-value-bind] variables are similarly inferred from the types of the
individual values of the values form.

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 @f[and] type specifier.  In this example:
@lisp
(defmacro my-dotimes ((var count) &body body)
  `(do ((,var 0 (1+ ,var)))
       ((>= ,var ,count))
     (declare (type (integer 0 *) ,var))
     ,@@body))

(my-dotimes (i ...)
  (declare (fixnum i))
  ...)
@endlisp
the two declarations for @f[i] are intersected, so @f[i] is known to be a
non-negative fixnum.

In practice, this type inference is limited to lets and local functions, since
the compiler can't analyze all the calls to a global function.  But type
inference works well enough on local variables so that it is often unnecessary
to declare the type of local variables.  This is especially likely when
function result types and structure slot types are declared.  The main place
where type inference breaks down is when the initial value of a variable is a
untyped expression, such as @f<@w<(car x)>>.

@section[Local Function Type Inference]

The types of arguments to local functions are inferred in the same was as any
other local variable; the type is the union of the argument types across
all the calls to the function, intersected with the declared type.  If there
are any assignments to the argument variables, the type of the assigned value
is unioned in as well.

@b[### Important for inferring return values count]

The result type of a local function is computed in a special way that takes
tail recursion into consideration.  The result type is the union of all
possible return values that aren't tail-recursive calls.  For example, @python
will infer that the result type of this function is @f[integer]:
@lisp
(defun ! (n res)
  (declare (integer n res))
  (if (zerop n)
      res
      (! (1- n) (* n res))))
@endlisp
Although this is a rather obvious result, it becomes somewhat less trivial in
the presence of mutual tail recursion of multiple functions.  Local function
result type inference interacts with the mechanisms for ensuring proper tail
recursion.

@section[Global Function Type Inference]
@label[function-type-inference]
@label[function-types]

@f[function] types are understood in the restrictive sense, specifying:
@begin[itemize]
The argument syntax that the function must be called with.  This is information
about what argument counts are acceptable, and which keyword arguments are
recognized.  In @python, warnings about argument syntax are a consequence of
function type checking.

The types of the argument values that the caller must pass.  If the compiler
can prove that some argument to a call is of a type disallowed by the called
function's type, then it will give a compile-time type warning.  In addition to
being used for compile-time type checking, these type assertions are also used
as output type assertions in code generation.  For example, if @f[foo] is
declared to have a @f[fixnum] argument, then the @f[1+] in @w<@f<(foo (1+ x))>>
is compiled with knowledge that the result must be a fixnum.

The types of the values that will be bound to argument variables in the
function's definition.  Declaring a function's type with @f[ftype] implicitly
declares the types of the arguments in the definition.  @python checks for
consistency between the definition and the @f[ftype] declaration.  Because of
precise type checking, an error will be signalled when a function is called
with an argument of the wrong type.

The type of return value(s) that the caller can expect.  This information is a
useful input to type inference.  For example, if a function is declared to
return a @f[fixnum], then when a call to that function appears in an
expression, the expression will be compiled with knowledge that the call will
return a @f[fixnum].

The type of return value(s) that the definition must return.  The result type
in an @f[ftype] declaration is treated like an implicit @f[the] wrapped around
the body of the definition.  If the definition returns a value of the wrong
type, an error will be signalled.  If the compiler can prove that the function
returns the wrong type, then it will give a compile-time warning.
@end[itemize]

So wherever a call to a declared function appears, there is no doubt as to the
types of the arguments and return value.  Furthermore, @python will infer a
function type from the function's definition if there is no @f[ftype]
declaration.  Any type declarations on the argument variables are used as the
argument types in the derived function type, and the compiler's best guess for
the result type of the function is used as the result type in the derived
function type.

This method of deriving function types from the definition implicitly assumes
that function result types won't be incompatibly redefined at run-time, since
calls are compiled as though the function will always return the same type that
the definition present at compile time returned.  For this reason, there is a
switch to suppress function type inference from definitions.

@section[Operation Specific Type Inference]
@label[operation-type-inference]

Many of the standard @clisp functions have special type inference procedures
that determine the result type as a function of the argument types.  For
example, the result type of @f[aref] is the array element type.  Here are some
other examples of type inferences:
@lisp
(logand x #xFF) ==> (unsigned-byte 8)

(+ (the (integer 0 12) x) (the (integer 0 1) y)) ==> (integer 0 13)

(ash (the (unsigned-byte 16) x) -8) ==> (unsigned-byte 8)
@endlisp

@section[Dynamic Type Inference]
@label[constraint-propagation]

Python uses flow analysis to infer types in dynamically typed programs.  For
example:
@lisp
(ecase x
  (list (length x))
  ...)
@endlisp
Here, the compiler knows the argument to @f[length] is a list, because the call
to @f[length] is only done when @f[x] is a list.

Dynamic type inference has two inputs: explicit conditionals and implicit or
explicit type assertions.  Flow analysis propagates these constraints on
variable type to any code that can be executed only after passing though the
constraint.  Explicit type constraints come from @f[if]s where the test is
either a lexical variable or a known predicate of lexical variables and
constants.

If there is an @f[eq] (or @f[eql]) test, then the compiler will actually
substitute one argument for the other in the true branch.  For example:
@lisp
(when (eq x :yow!) (return x))
@endlisp
becomes:
@lisp
(when (eq x :yow!) (return :yow!))
@endlisp
This substitution is done when one argument is a constant, or one argument has
better type information than the other.  This transformation reveals
opportunities for constant folding or type-specific optimizations.  If the test
is against a constant, then the compiler can prove that the variable is not
that constant value in the false branch, or @w<@f<(not (member :yow!))>>
in the example above.  This can eliminate redundant tests, for example:
@lisp
(if (eq x nil)
    ...
    (if x a b))
@endlisp
is transformed to this:
@lisp
(if (eq x nil)
    ...
    a)
@endlisp
Variables appearing as @f[if] tests are interpreted as 
@f[@w[(not (eq @i[var] nil))]] tests.  The compiler also converts @f[=] into
@f[eql] where possible.  It is difficult to do inference directly on @f[=]
since it does implicit coercions.

When there is an explicit @f[<] or @f[>] test on integer variables, the
compiler makes inferences about the ranges the variables can assume in the true
and false branches.  This is mainly useful when it proves that the values are
small enough in magnitude to allow open-coding of arithmetic operations.  For
example, in many uses of @f[dotimes] with a @f[fixnum] repeat count, the
compiler proves that fixnum arithmetic can be used.

Implicit type assertions are quite common, especially if you declare function
argument types.  Dynamic inference from implicit type assertions sometimes
helps to disambiguate programs to a useful degree, but is most noticeable when
it detects a dynamic type error.  For example:
@lisp
(defun foo (x)
  (+ (car x) x))
@endlisp 
results in this warning:
@lisp
In: DEFUN FOO
  (+ (CAR X) X)
==>
  X
Warning: Result is a LIST, not a NUMBER.
@endlisp

Note that @llisp's dynamic type checking semantics make dynamic type
inference useful even in programs that aren't really dynamically typed, for
example:
@lisp
(+ (car x) (length x))
@endlisp
Here, @f[x] presumably always holds a list, but in the absence of a declaration
the compiler cannot assume @f[x] is a list simply because list-specific
operations are sometimes done on it.  The compiler must consider the program to
be dynamically typed until it proves otherwise.  Dynamic type inference proves
that the argument to @f[length] is always a list because the call to @f[length]
is only done after the list-specific @f[car] operation.

The most significant efficiency effect of inference from assertions is usually
in type check optimization.


@section[Type Check Optimization]
@label[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:
@lisp
(defstruct foo a b c)
(defstruct link
  (foo (required-argument) :type foo)
  (next nil :type (or link null)))

(foo-a (link-foo x))
@endlisp
Here, there is no need to check that the result of @f[link-foo] is a @f[foo],
since it always is.  Even when some type checks are necessary, type inference
can often reduce the number:
@lisp
(defun test (x)
  (let ((a (foo-a x))
	(b (foo-b x))
	(c (foo-c x)))
    ...))
@endlisp
In this example, only one @w<@f<(foo-p x)>> check is needed.  This applies to a
lesser degree in list operations, such as:
@lisp
(if (eql (car x) 3) (cdr x) y)
@endlisp
Here, we only have to check that @f[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
@f[car] and @f[cdr]:
@lisp
(defun memq (e l)
  (do ((current l (cdr current)))
      ((atom current) nil)
    (when (eq (car current) e) (return current))))
@endlisp

Python reduces the cost of checks that must be done through an optimization
called @i[complementing].  A complemented check for @i[type] is simply a check
that the value is not of the type @w<@f<(not @i[type])>>.  This is only
interesting when something is known about the actual type, in which case we can
test for the complement of @w<@f<(and @i[known-type] (not @i[type]))>>, or the
difference between the known type and the assertion.  An example:
@lisp
(link-foo (link-next x))
@endlisp
Here, we change the type check for @f[link-foo] from a test for @f[foo] to a
test for:
@lisp
(not (and (or foo null) (not foo)))
@endlisp
or more simply @w<@f<(not null)>>.  This is probably the most important use of
complementing, since the situation is fairly common, and a @f[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:
@lisp
(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)))))
@endlisp
This loop can be compiled with no type checks.  The @f[link] test for
@f[link-foo] and @f[link-next] is complemented to @w<@f<(not null)>>, and then
deleted because of the explicit @f[null] test.  As before, no check is
necessary for @f[foo-a], since the @f[link-foo] is always a @f[foo].  This sort
of situation shows how precise type checking combined with precise declarations
can actually result in reduced type checking.


@section[Rambling]

Much of the past work on unique overheads of @llisp (hence possible @llisp
hardware) has concentrated on the costs of dynamic type checking and
dispatching.  But Python's type check optimization substantially reduces the
cost of any necessary run-time type checking, and type inference and efficiency
notes minimize unnecessary run-time type dispatching.  The combination of this
sort of optimization with the technological advantage of using a
state-of-the-art mass-market microprocessor gives better cost/performance with
@i[better] safety that that given by a special-purpose processor with tag
checking hardware.

RISC architectures are actually a better fit for Lisp than conventional CISC
architectures, since conventional complex architectural features (call
instruction, etc.) are rarely usable in a @llisp implementation.  It seems that
the main area for progress in support for symbolic programming is not so much
the instruction set architecture as the memory architecture.