Types in CL

[Barry Margolin <barmar@Think.COM>]

    Date:     Thu, 17 Dec 87 10:48:05 PST
    From: Jeff Barnett <jbarnett@nrtc.northrop.com>

    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)).

By doing (SETF (AREF A 0) A) you have violated the type declaration you
specified, because you said that the elements of the array would never
be of the same type as the array itself, so a compiler would be
justified in assuming that (EQ A (AREF A 0)) is never true.

    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.

Look up Russell's paradox (the one about the barber who shaves all and
only people who don't shave themselves, or the catalog of all books not
in any other catalog) in a logic book.  Any sufficiently expressive
class system allows such classes to be specified, even though such sets
cannot actually exist because they are self-contradictory.  Your example
isn't really like this, because the Lisp type system lacks the ability
to specify that an array of type T1 contains ALL objects of type T2.

                                                barmar