Re: Issue: DECLARE-TYPE-FREE (Version 9)

[Kent M Pitman <KMP@STONY-BROOK.SCRC.Symbolics.COM>]

    Date: 5 Jan 89 22:14 PST
    From: masinter.pa@Xerox.COM

    The example I keep coming back to is one where it isn't so much that the
    local declaration is easy to enforce as it is where it is difficult *not*
    to enforce it.

    Suppose I have

    (defun frob (delta)
     (flet ((more (x) (+ x delta)))
	    ;; if you like, put (declare (inline more)) here
       (typecase delta
	    (float (locally (declare (type float delta))
		    ... (more rho ) ... ))

	   ((signed-byte 8)
		    (locally (declare (type (signed-byte 8) delta))
		    ... (more zz) ... ))
	...)))

[Parens added.]

    Even without the inline, it is a common & legal transformation to do inline
    substitution on "small" fletted functions.

Absolutely. But not textually. Semantically. For example, you already
have to watch for:

(defun add (x y) (+ x y))

(defun frob (delta)
  (flet ((more (x) (add x delta)))
    (flet ((add (x y) (- x y)))
      ... (more x) ...)))

    Even though the reference "delta" in the definition of more isn't
    within the lexical scope of the local declaration, it *is* the same
    delta.

Right. But that itself implies nothing.

    While its not impossible to maintain a separate contour in order to
    segregate the type declarations, it seems like unnecessary work, 

It is not unnecessary. You cannot just substitute a piece of unadorned
text. You have to do the substitution at a lower level using an adorned
call tree or else you have to have resolved out all the relevant lexical 
things before you start merging source (ie, you have to have assured that
the flet problem is not going to happen). If your approach is the former,
it's possible (maybe even "easy" or at least "standard practice") to
represent every reference to a variable with a pointer to the lexical
environment it came from, so you can get the lookup right. If your
approach is the latter, then it's possible to make all the declarations
explicit as you do the code-walk looking for flets and whatnot so that
you don't have to rely on DECLARE info afterward. In that case, the result
of your traversal should be:

 (defun frob (delta)
   (typecase delta
     (float ... ((lambda (x) (+ x delta)) rho) ...)
     ((signed-byte 8)
      ... ((lambda (x) (+ x delta)) zz) ... )
     ...))

    ... and in fact, the declaration is quite useful if "more" is inlined.

Actually, in this case it doesn't provide any information that
the compiler can't figure out from the TYPECASE. A good compiler
is not limited in its type inferencing to what has been declared.
It can tell that no SETQ is going on, so it can propagate the type
 from the TYPECASE directly without even the aid of the DECLARE.

Let's look at a better example which is opaque to the compiler:

(defun frob (n m)
  (frob1 (cond ((and (typep n 'fixnum) (typep m 'fixnum)) 'fixnum)
	       ((and (typep n 'float)  (typep m 'float))  'float)
	       (t 't))
	 n m))

(defun frob1 (type n m)
  (flet ((zap () (+ n m)))
    (case type
      (fixnum (locally (declare (fixnum n m)) (zap)))
      (float  (locally (declare (float  n m)) (zap)))
      (otherwise (zap)))))

In this case, I agree you're potentially losing some slight amount
of efficiency, but ...

 (a) You could use MACROLET instead to get back that efficiency.
     I personally believe that it is stylistically the correct
     thing for this situation.

 (b) There is a twin brother of this example which I don't want to
     let through, and which your proposal would force me to reckon
     with:

     (defun frob (n m)
       (frob1 (cond ((and (typep n 'fixnum) (typep m 'fixnum)) 'fixnum)
		    ((and (typep n 'float)  (typep m 'float))  'float)
		    (t 't))
	      #'(lambda () 
	          (declare (special n m))
		  (let ((nn n) (mm m))
		    (setq n nil m nil)
		    (setq n nn  m mm)
		    (+ n m)))
	      n m))
     
     (defun frob1 (type fn n m)
       (declare (special n m))
       (flet ((zap () (funcall fn)))
	 (case type
	   (fixnum (locally (declare (fixnum n m)) (zap)))
	   (float  (locally (declare (float  n m)) (zap)))
	   (otherwise (zap)))))

     In your interpretation, this code is in error, while in my
     interpretation, this code is valid. I consider it a gross
     modularity violation for the effect of a type declaration to
     have other than lexical scope.

     The only alternatives seem to me to be:

	- Don't do local type declarations on special variables.
	  [This costs efficiency in other places, so your proposal
	   would be trading one kind of efficiency barrier for
	   another.]

	- Scope type declarations for special variables differently
	  for lexical and dynamic variables. Curiously, you would
	  have lexical variables enforce their type declarations
	  dynamically, and dynamic variables enforce their type
	  declarations lexically.

	- Scope all type declarations lexically.

     The only one I have any support for is still the third, which
     is Moon's LEXICAL proposal.