Types in CL

[Jeff Barnett <jbarnett@nrtc.northrop.com>]

Recently, there has been some message traffic concerning functional type
specification and related topics.  The purpose of this note is to point
out two problems with the CL type mechanism that I have not seen
discussed: the first concerns a case were the value of TYPEP *must* be
undefined and the second concerns the definition of a subtype of a
functional type.

PROBLEM I.  Assume that the following have been evaluated
	(DEFTYPE T1 '(ARRAY T2 1))
	(DEFTYPE T2 '(NOT T1))
Let A be a one-dimensional array of size 1 such that (EQ A (AREF A 0)).
What should the value of (TYPEP A 'T1) be?  It is easy to see that A is
in type T1 if and only if it is not in type T1.  A type specification
mechanism that allows (1) recursive definitions and (2) a negation
operation is sure to have this problem.  Obviously, we want recursive
specification so that chains or rings of same-typed structures can be
specified and we want negation so that the programmer does not need to
explicitly list every possible alternative type in his definition.

PROBLEM II.  Assume that the following return non-NIL
	(SUBTYPEP 'T1 'T2)
	(SUBTYPEP 'T2 'T3)
The question is what are the subtypes of the type specifier
	(FUNCTION (T2) T2)
I think that the answer is
	(FUNCTION (T3) T1)
because the type-specific contract of an F in type (FUNCTION (T2) T2) is
to (1) accept as arguments objects in T2 and (2) return objects in T2.
Therefore, an F that accepts objects in T3 (which includes all of T2)
and returns objects in T1 (all of which are in T2) satisfies that
contract.  An F in (FUNCTION (T1) T3) does not because (1) it does not
promise to handle an object in T2-T1 and (2) may return an object in
T3-T2.  Therefore,
	(SUBTYPEP '(FUNCTION (T3) T1) '(FUNCTION (T2) T2))
should be non-NIL while
	(SUBTYPEP '(FUNCTION (T1) T3) '(FUNCTION (T2) T2))
should be NIL.  Note, as SUBTYPEP decomposes functional type
specifications and recurs, it must *reverse* the order of its arguments
when checking argument types---original order is used when value types
are checked.  It is somewhat amusing to trace a case where the type
specification of either the arguments and/or the values are themselves
functional types or where functional types are recursively specified.

One reason to make sure that determining subtype-ness of functional
types is as accurate as it can be as often as possible arises because
most LISPS do incremental compilations and are interactive.  If a
function is recompiled and either its argument or value types change, it
would be good to inform the user where there are calls that are no
longer type-compatible.  IF THE NEW TYPE OF THE FUNCTION IS A SUBTYPE OF
THE OLD, THEN, AS FAR AS TYPE CHECKING IS CONCERNED, EVERYTHING MUST BE
OKAY.  It is only when this is not true, that it is necessary to check
the types of objects actually passed to the function from other code or
see what assumptions have been made in consuming the returned objects.

There is a slight generalization of the comments as to what is a
reasonable definition of subtype of functional types.  Assume that a
variable or register has been given a type specification.  Let that type
specification be changed.  There are three possibilities:
1. THE NEW TYPE SPECIFICATION IS A SUBTYPE OF THE OLD
	Code that only reads the cell is not affected.
	Code that writes the cell may or may not be valid.
2. THE NEW TYPE SPECIFICATION IS A SUPERTYPE OF THE OLD
	Code that only writes the cell is not affected.
	Code that reads the cell may or may not be valid.
3. THE NEW AND OLD TYPE SPECIFICATIONS ARE NOT COMPARABLE
	Any code that reads the cell may or may not be valid.
The reason that the above implies the rules for functional subtype
determination is that, from the point of view of a function caller,
arguments represent write-only registers while values represent
read-only registers.  A while ago, there was some discussion of having a
class of read-only goodies in LISP.  If that is ever sanctioned, these
comments may provide some guidance in error checking interactions of
that mechanism with type declarations and revisions.
	Jeff