Re: Types in CL

[Barry Margolin <barmar@think.com>]

    Date:     Thu, 17 Dec 87 12:56:57 PST
    From: Jeff Barnett <jbarnett@nrtc.northrop.com>

    Your claim that the compiler should inhibit (SETF (AREF A 0) A) is only valid 
    if A is declared of type T1.  

I never said anything about the compiler inhibiting the SETF.  I said
that it is incorrect to do the SETF.  However, you are correct that I
was wrong; you didn't show the MAKE-ARRAY form, and I assumed A was
created with

	(setq a (make-array 1 :element-type 't2))

				  It may not be.  What you are pointing out is
    that there is a problem if one tries to determine the type of an object (or
    its type membership status) *after* the object is created.

Actually, there is a bug in your original message, in the TYPEP call.
The predicate

	(TYPEP A 'T1)

expands to

	(TYPEP A '(ARRAY T2 1))

which is equivalent to

	(AND (ARRAYP A)
	     (EQ (ARRAY-ELEMENT-TYPE A) 'T2)
	     (= (ARRAY-RANK A) 1)
	     (= (ARRAY-DIMENSION A 0) 1))

Note that it never does an AREF, so the question of whether (AREF A 0)
is of type T2 never comes up.  When array types are used in TYPEP, the
element type does not refer to the current contents, but to the array's
implementation type.

In order to create the type anomaly you describe, you must use the
SATISFIES type specifier, e.g.

(DEFUN T1P (A)
  (AND (ARRAYP A)
       (= (ARRAY-RANK A) 1)
       (= (ARRAY-DIMENSION A 0) 1)
       (TYPEP (AREF A 0) 'T2)))

(DEFTYPE T1 () '(SATISFIES T1P))

When you do this, (TYPEP A 'T1) is guaranteed to infinitely recurse.
Because Lisp's type system permits arbitrary code to be incorporated,
the type system is Turing-equivalent, which means that the halting
problem exists.  Without SATISFIES, though, the problem you describe
doesn't exist, because none of the other type specifiers require doing a
TYPEP of constituents of the object being tested (actually, I think
(TYPEP A '(COMPLEX <type>)) is an abbreviation for

	(AND (COMPLEXP A)
	     (TYPEP (REALPART A) '<type>)
	     (TYPEP (IMAGPART A) '<type>))

but no recursion can occur because the parts of a complex number cannot
be complex).

                                                barmar