> Of course, in the absence of some unusual 
> limitation on the expressive power of array creation and 
> indexing expression, the general problem of static detection 
> of array indexing errors is undecidable.

Indeed.

> I wonder if the compiler gurus at the INRIA know what kinds 
> of constraints imposed on the language would allow the 
> compiler to statically check array indexing.

Well, for this purpose, array index expressions must be restricted to
a sub-language where inequations between index expressions are
decidable.  A well-known such sub-language is Presburger arithmetic:
index expressions are variables, constants, and sums and products of
expressions.  I don't know of any significantly more expressive
sub-language that has the required decidability properties.

> I can imagine a few applications, such as signal analysis, where the
> program logic is simple enough that such a restricted language might
> suffice, and come to the aid of the developer who presently uses
> unsafe arrays for the sake of speed, but with no help from the
> compiler at prooving that the program is correct with respect to
> array indexing.

Obligatory preliminary remark: the cost of run-time array bound checks
is not that high, since on modern processors it is performed
largely in parallel with the actual array access.  On my tests,
ocamlopt -unsafe is at best 25% faster than ocamlopt on array
intensive programs.

This said, the approach you outline was investigated in depth by
Hongwei Xi in his work on Dependent ML:

        http://www.ececs.uc.edu/~hwxi/DML/DML.html

It's an interesting reading.

- Xavier Leroy
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners