[Gcl-devel] Re: Looking for a good type propagation algorithm

[Paul F. Dietz]

Camm Maguire wrote:
> Greetings!  As many may know, GCL autodeclares constant let bindings,
> and this allows for many optimizations to proceed.  We could also
> autodeclare bindings which are changed, but changed to a subtype of
> the original type, let alone autodeclaring loop counters after
> checking loop bounds, etc.  
>
> The problem is that I cannot think of a decent algorithm which is not
> exponential in the let form nesting.  I.e., start by setting the
> variable types to the type of the initializing form in the outermost
> let, then using these settings, do likewise for all sub-lets, until
> one hits the setq, at which point one can determine whether the setq
> preserves the type.  Otherwise, mark the type as t (could
> alternatively iterate with `(or ,type ,setq-type)), and then process
> the outer let for real.  The outermost let is processed twice, the
> next innermost four times, etc.
>
> Anyone know of a better algorithm?  I was thinking about just one
> pass, and building up a network of linked type-setter functions as you
> go, but this appears too ambitious at present.


You might be thinking of something like Abstract Interpretation.
In this technique, the values that some program constract may have
are approximated by some element of a lattice of finite height.
When a variable can have more than one possible value, the lattice
element is the join (least upper bound) of the lattice elements
for those values.

If there are n such values (corresponding to the variables
and forms of the program, say), you get a set of equations
of the form

  v_i = \/ f_{i,j}(v_1,...,v_n)

where f_{i,j} is a function on the lattice values that is continuous
in the lattice (that is, moving one of its arguments up in the lattice
causes the value of the function to either remain the same or also
move up.)

The fixpoint of this system of equations can be found in O(n height(L))
function evaluations, where height(L) is the height of the lattice, by
the obvious algorithm of starting variables with bottom values and propagating
changes around the graph.

In our case, the lattice would be some approximation of Lisp's type
system, since lisps full type system is not finitely high (and
even limited integer subrange types would lead to exponentially
high lattices.)

        Paul