> 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,

I'm afraid that this is not so easy, especially under separate
compilation.  For example, if we want to separately-compile a function
like "fun ref x -> !x + 1" (in the ocaml syntax), and if x could be
null, then the null check elimination would be hard.  Such situations
seem ubiquitous in practice.

On the other hand, ML types work as an interface to specify whether x
is always initialized ("int ref") or not ("int option ref").  And
static typing enforces such a protocol between modules.

> Note that Java is imperative, which makes flow analysis easier
> (compared to ML).

I wonder how flow analysis can be easier in Java than in ML.  While ML
has higher-order functions, Java has inner classes.

> A common saying is that a program is made safer if references
> are always initialized. I find this is contrary to the truth.
> In this case, a program is made safer if you insert run-time
> checks (and rely on a compiler to remove redundant checks)
> 
> If I use 'get' and 'set', is there a compiler to eliminate such
> checks (i.e., after 'set', 'get' should do no tag checking)?
> 
> Yes, ML allows the programmer to tag values (using option
> types) and thus shifts the burden to the programmer. In Java,
> this is done automatically (and we can rely on a compiler to
> remove redundant null checks).

ML could also do it automatically, by analyzing whether a value of an
"option" type always has the "Some" tag.  The analysis would be
similar to standard flow analyses or type-based analyses.

// Eijiro Sumii <sumii@saul.cis.upenn.edu>
//
// currently visiting: Department of Computer and Information Science,
// School of Engineering and Applied Science, University of Pennsylvania