gcl-devel
[Top][All Lists]

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

 From: Paul F. Dietz Subject: [Gcl-devel] Re: Looking for a good type propagation algorithm Date: Sat, 17 Sep 2005 20:21:12 -0500 User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.11) Gecko/20050729

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