LISP and Symbolic Computation, 5(3)157-190
A Decision Procedure for Common Lisp's SUBTYPEP PredicateHenry G. Baker, Nimble Computer Corporation, 16231 Meadow Ridge Way, Encino, California 91436
|
Abstract: Common Lisp [25], [26] includes a dynamic datatype
system of moderate complexity, as well as predicates for checking the
types of language objects. Additionally, an interesting predicate of
two "type specifiers"-- SUBTYPEP--is included in the language. This
subtypep predicate provides a mechanism with which to query the Common
Lisp type system regarding containment relations among the various
built-in and user-defined types. While subtypep is rarely needed by an
applications programmer, the efficiency of a Common Lisp
implementation can depend critically upon the quality of its subtypep
predicate: the run-time system typically calls upon subtypep to decide
what sort of representations to use when making arrays; the compiler
calls upon subtypep to interpret user declarations, on which efficient
data representation and code generation decisions are based. As might be expected due to the complexity of the Common Lisp type system, there may be type containment questions which cannot be decided. In these cases subtypep is expected to return "can't determine", in order to avoid giving an incorrect answer. Unfortunately, most Common Lisp implementations have abused this license by answering "can't determine" in all but the most trivial cases. In particular, most Common Lisp implementations of SUBTYPEP fail on the basic axioms of the Common Lisp type system itself [25][26]. This situation is particularly embarrassing for Lisp--the premier "symbol processing language"--in which the implementation of complex symbolic logical operations should be relatively easy. Since subtypep was presumably included in Common Lisp to answer the hard cases of type containment, this "lazy evaluation" limits the usefulness of an important language feature. This paper shows how those type containment relations of Common Lisp which can be decided at all, can be decided simply and quickly by a decision procedure which can dramatically reduce the number of occurrences of the "can't determine" answer from subtypep. This decision procedure does not require the conversion of a type specifier expression to conjunctive or disjunctive normal form, and therefore does not incur the exponential explosion in space and time that such a conversion would entail. The lattice mechanism described here for deciding subtypep is also ideal for performing type inference [2]; the particular implementation developed here, however, is specific to the type system of Common Lisp [4]. Categories and Subject Descriptors: Lisp, dynamic typing, compiler optimization, type inference, decision procedure. |
This article is not available online.