Issue: DECLARE-TYPE-FREE (Version 6)

[jar@void.ai.mit.edu (Jonathan Rees)]

I can't figure out at all what DECLARE-TYPE-FREE:ALLOW is supposed to mean.

    From: Masinter.PA@Xerox.COM, KMP@STONY-BROOK.SCRC.Symbolics.COM
    Subject: Issue: DECLARE-TYPE-FREE (Version 6)
    To: X3J13@SAIL.Stanford.EDU

[A]   ... Clarify that a type
      declaration means that it is an error for the value of the variable not
      to be a member of the declared type, within the scope of the declaration.

[B]   Clarify that the above programs are valid, and that this  kind of 
      declaration means the same thing as wrapping a THE form around every 
      reference to the variable, including modifying references by setq or
      setf.
      Clarify that if nested type declarations refer to the same variable, then
      the value of the variable must be a member of the intersection of the 
      declared types.

The phrase "within the scope of the declaration" in [A] is in direct
conflict with the explanation that follows [B].  If "scope" means
"lexical scope", then the following would be an error according to [A]
but not according to [B]:

	(let ((x 12) (y 'foo))
	  (flet ((zap () (rotatef x y)))
	    (locally (declare (fixnum x))
	      (zap)
	      (zap)
	      x)))

Here the declaration is violated at the "lexical" point in the program
between the two calls to ZAP.  If "scope" means "dynamic scope", you
still have a problem with

	(let ((x 12) (y 'foo))
	  (flet ((zap ()
		   (rotatef x y)
		   (rotatef x y)))
	    (locally (declare (fixnum x))
	      (zap)
	      x)))

since now there is one point *dynamically* where the declaration is
violated.

In either case, this seems like a tricky thing for a compiler to
attempt to understand, and also pretty tricky for an interpreter (and
in particular, a formal semantics) to enforce.  I would think that
recovering the needed information via data flow would be easier.

Even if you decide to trash definition [A] and go with definition [B],
I would think that you'd additionally want to specify that the
declaration must hold not only at all references and assignments
lexically in the scope of the declaration, but also at the point of
the declaration itself.  Consider the case where the variable is
unreferenced in the body; then the declaration wouldn't tell you a
thing, and e.g. it wouldn't help you with backward flow analysis.  Or
the variable might be referenced, but the declaration might not become
valid until some time a while after the point of the declaration:

	(let ((x 'foo))
	  (flet ((zap () (setq x 17)))
	    (locally (declare (fixnum x))
	      (zap)
	      x)))

Also, what does the declaration mean for non-lexical variables?  Would
it apply dynamically to any dynamic binding or reference in the
dynamic scope of the declaration, or just to the references to the
particular dynamic binding that was in effect at the point of
declaration, or just to lexically apparent references in the lexical
scope of the declaration?

I would strongly oppose the proposal in its current vague form.  I
think I would oppose the proposal in just about any form, because it
makes the semantics of variable references even more hairy than it
already is.  Compilers ought to recover this kind of information from
data flow analysis, assisted if necessary by assertions (e.g. uses of
THE in for-effect positions).