Re: CMU CL 15c performance

["Thomas M. Breuel" <tmb@ai.mit.edu>]

|Python will infer that a DOTIMES (or other loop with a fixnum count and a
|inequality exit test) ranges only over fixnums.  However, due to
|limitations of the current flow analysis algorithm, it is confused when
|the body contains a nested loop.  Ideally it should also infer that a
|bounds check is unnecessary, but I haven't even thought about how to do that.

What about pulling out _all_ array bounds checks from DOTIMES and
similar loops:

	(dotimes (i n) ... (aref a i) ...)

	=>

	(assert (>= (array-dimension a 0) n))
	(dotimes (i n) ... (unchecked-aref a i) ...)

Then, the compiler could eliminate any assertion that is obviously
true. 

I don't know what the semantics of CommonLisp errors are; if an
implementation is not allowed to signal an error early (i.e.,
before all side-effects leading up to the error have been carried 
out), I think the semantics are wrong. But even then, it would
probably be profitable to convert this into something like:

	(cond ((>= (array-dimension a 0) n)
	       (dotimes (i n) ... (unchecked-aref a i) ...))
	      (t
	       (warning "I'm going to signal an error real soon now...")
	       (dotimes (i n) ... (aref a i) ...)))


|Hmmmn.  I would guess that MIN did work.  However, there is a problem with
|arithmetic operators like +, *, etc.  The initial result type assumption
|for these operators is NUMBER.  In order to realize that the value is
|always a float, it would have to first postulate that the value was a float
|and then see if this solution were consistent, in effect do an inductive proof.

Couldn't you express the fact that (+ <single-float> <single-float>)
must always yield a <single-float>? This sort of comes back to the
"polymorphic constraint" question below.

|Dynamic type inference is a somewhat subtle thing.  Python will infer that
|the value is a FIXNUM, but only downstream of the array reference.
|Sometimes this is enough to prove that a loop variable is a fixnum, and
|sometimes not.  In a dynamically typed language one can write:
|    (dotimes (i n)
|      (if (typep i 'fixnum)
|	  (aref v i)
|	  (write-line "We got a big one!")))

Yes, but in my case, there were no conditionals, type predicates, or
assignments to "i". I think it would be very useful if such type
constraints could propagate backwards since this is a very common 
case.

For example, in the case of

	(dotimes (i n)
	  (foo i)
	  (bar (aref v i)))

it seems to be legal to infer that "i" must be a fixnum (and smaller
than (array-dimension v 0)), or else the program is in error. The same
comments about errors and side-effects as above also apply here, of course:
I don't know whether the implementation can signal the error early. But
it can always generate two loops: an efficient one that uses fixnums,
and an unoptimized one that may even warn about the impending error
condition before all side-effects have occurred.

|The idea of explicitly declaring polymorphic types is an interesting one,
|and would probably fit better in Common Lisp and a ML-like inference
|scheme.  One semantic problem is the need to define what it means to be
|"the same type" when you are substituting in a pattern.

Probably, the most natural style of declaration would say something
like "when applied to two single-float values, this function yields
a single float". Again, the CL type system is a little too subtle for
me to know whether that can be expressed within the current
type system, but I think Lucid used to interpret FTYPE declarations 
like this.

				Thanks, Thomas.