Issue: DECLARATION-SCOPE (Version 2)

[Ram@C.CS.CMU.EDU]

    Date: Monday, 8 February 1988  13:57-EST
    From: Kent M Pitman <KMP at STONY-BROOK.SCRC.Symbolics.COM>
    To:   Moon at STONY-BROOK.SCRC.Symbolics.COM
    Re:   Issue: DECLARATION-SCOPE (Version 2)

    [...] I wonder about the following cases.

I don't understand the unclarity that you seem to perceive in the
rules for scoping.  We may not agree on what the lexical scope for
DECLARE should be, but I think we all agree that it is lexical.  A
DECLARE at the head of a DEFUN (or lambda, or let, or anything else)
shouldn't affect anything outside of the body.  The only
pseudo-exception is macros, which are known to violate referential
transparency.

    (DEFUN FOO-1 (X)
      (DECLARE (INLINE FOO-1))
      (+ X 1))

    (DEFUN BAR-1 (X) (FOO-1 X))

    Can FOO-1 be inlined in BAR-1?

No, because the call to FOO-1 isn't within the scope of the
declaration.

    [...]  I think there are implementations which do this inlining. I
    would like to see this and other situations treated explicitly.

I agree, and in my compiler cleanup proposal I have treated the
concept of compile-time function binding (which inlining is a special
case of) at some length.

    (DEFUN BAR-2 (X)
      (FLET ((FOO-2 (X)
    	   (DECLARE (INLINE FOO-2))
    	   (+ X 1)))
        (FOO-2 X)))

    Can FOO-2 be inlined in BAR-2? I say it's not totally unreasonable
    and I wouldn't be surprised if some implementations have resorted to
    this [...]  Is this right? Can we get this into the spec?

Yes, but not for the reason you say.  A lexical function can be called
however the compiler bloody well wants to, since there is no way that
the user can ever redefine it.  If the compiler happens to take a
spurious declaration as a cue, that's fine, but it could just as well
use the phase of the moon.  But once again, it is clear that the
INLINE declaration doesn't affect the function FOO-2 that you are
talking about, it is allowing inline expansion of some other FOO-2
(presumably global) within the body of the lexical FOO-2.

    [...]
    (DEFUN FOO-3 (X)
      (DECLARE (FUNCTION FOO-3 (FIXNUM) FIXNUM))
      (+ X 1))

    Can I use fixnum arithmetic in FOO-3? (I say yes.)

I don't think so, although this rides on a combination of
interpretations of sticky points: function types in general, and
pervasive function type declarations in particular.

First of all, function type semantics require that the compiler prove
that the argument is a fixnum before it can assume that the result is
a fixnum.  This means that even a global function type declaration is
useless when compiling the body, since there is no way the compiler
can convince itself it has seen all possible calls.

Secondly, the interpretation of the pervasive function type
declarations is really unclear, especially in the absence of any calls
within the scope.  It seems that what you are saying is that within
this scope (but perhaps not elsewhere), FOO-3 will return a fixnum
when given a fixnum.  If the compiler could prove that a declaration
that is true in this scope would be true in any scope (here
plausible), then this type declaration could perhaps be applied to
other calls, but only when the compiler could be sure that the same
FOO-3 was being referred to, which is difficult given the lack of a
general mechanism for allowing compile-time resolution of global
function names.  But the fact that there is no call to FOO-3 within
the scope leads one to wonder whether any random declaration might be
vacuously true.

As I have said before, I think that the concept of function type in
Common Lisp (as correctly interpreted) is fairly useless.  In my
compiler cleanup proposal, I handle compile-time function typing as a
special case of compile-time function binding.

If you have a proclamation that says all gloabal references to a
function are to a version that has been processed by the compiler,
then the compiler can propagate the types declared for the formal
parameter variables to the actual calls.  The compiler is free to use
whatever type-inference method it pleases to determine the result
type.

The other examples you gave seem to refelect a similarly perplexing
interpretation of pervasive function type declartions.

  Rob