> [The Java solution with null pointers]
> Yes, in theory, it requires null check at every use. However,
> I assume that a marjority of such null checks can be readily
> eliminated using flow analysis, though things can become difficult
> when arrays are involved. Note that Java is imperative, which
> makes flow analysis easier (compared to ML).

Don't count too much on the Java compiler being able to eliminate null
checks.  I don't think today's Java compiler technology is good enough
to do that.  Also:

- To eliminate null checks efficiently requires global (whole program)
analysis, which is nearly unapplicable to Java due to dynamic class
loading.
- To eliminate null checks for pointers fetched from an array requires
very subtle analyses, e.g. you need to keep track of which array
elements were initialized with non-null references and which elements
still hold the default null value.  (See below.)
- Those null checks work for arrays of objects, but not for arrays of
numerical quantities, which are initialized with default values just
like in ML.

This whole discussion seems to be going in circles.  If you want the
additional safety of run-time checking for uninitialized array
entries, you can get it in Caml by using option types, at a
performance cost.  If you'd rather avoid the performance cost, you
have to be a little more careful in your coding.  Finally, in many
cases you can have your cake and it eat too by avoiding low-level
operations such as "allocate array then fill it" and using
higher-level operations such as "tabulate this function in an array"
(a la Array.init).

Knowing the background of Hongwei Xi, I think I've guessed where he is
getting at: one could envision a refined type system for arrays that
keep track of (a conservative estimate of) the indices of elements
that have been initialized.  TAL does it for heap-allocated tuples,
and it would be interesting to see whether DML-style dependent types
allow such a type-checking for the more general case of arrays.
So, Hongwei, we'll read your next paper on this topic with interest :-)

My gut feeling about this approach is that the type system could
probably work well for arrays that are initialized linearly, e.g.

        let a = Array.create n in
        for i = 0 to n - 1 do
          a.(i) <- ...
          (* at this point, the type system knows that 
             a.(0)...a.(i-1) are initialized and
             a.(i)...a.(n-1) are not *)
        done
        (* at this point, the type system knowns that all elements of a
           are initialized *)

But notice that most of these cases are easily expressed using Array.init!

However, the type system is going to break horribly on more complex
initialization patterns, e.g. the following code for tabulating the
inverse of a permutation f over [0...n-1] :

        let a = Array.create n in
        for i = 0 to n - 1 do a.(f(i)) <- i done

So, I don't think the (Caml) programmer will gain much from a type
system/static analysis for array initialization.  (For a lower-level
language such as TAL, the story may be different, though.)

- Xavier Leroy