Re: type safety
On Mon, 10 Jan 2000, Joe Wells wrote:
> type safety: safety (for one program or for an entire programming
> language) enforced by requiring well typedness in some type
> * Some people might define safety to also require the absence of
> uncatchable exceptions. However, as long as these
> uncatchable exceptions generate well defined behavior (e.g.,
> halting), I think it is better to consider them safe.
Joe, I infer from these statements, together with the fact
that we can't tell at compile time whether an array index is in
bounds, that any language which does not check array bounds
dynamically cannot be type-safe. Is my inference correct? If not,
how are such languages handled in your view?
There are a few points which need to be made in response to this.
1. It is not so clear that it is a "fact that we can't tell at compile
time whether an array index is in bounds". While it is undecidable
in general whether a particular program will use an out-of-bounds
array index (by a simple reduction from the halting problem), we
can tell for many programs whether this is the case.
Furthermore, various type systems can be designed which can
represent proofs that out-of-bound array indexes are not used.
These type systems can guarantee programs only use in-bounds
indexes when accessing arrays. The papers mentioned earlier by
Hongwei Xi describe such type systems. It is possible using such a
type system to have safety without dynamic array bounds checks.
The difficulties of course are that (1) these type systems tend to
be complicated and (2) they can not handle some safe programs.
2. A language which does not verify (whether statically or dynamically)
that array indexes are in bounds is not safe at all.
3. Consider a programming language PL which does not dynamically
verify that array indexes are in bounds. Let "sub" be the operator
of PL such that sub(A,I) evaluates to the Ith element of array A,
if 0 <= I < length(A), and otherwise has undefined behavior when
evaluated (e.g., returns strange value, core dumps due to bus
error, runs lethal electric current through the nearest keyboard,
launches nearest nuclear-warhead-tipped missile, etc.).
The important question now is: What is the type of "sub"? Suppose
PL's type system assigns the following type to "sub":
sub : forall 'a . ('a array * int) -> 'a
This forall-quantified type can be instantiated, replacing 'a by
any other type. If this is the type of "sub", then this implies
that the meaning of _every_ type (any type that can be substituted
for 'a) includes "can have any behavior". Hence no types of PL
guarantee safety if the above type is used for "sub".
In order for PL to have a type system that guarantees safety, it
will need to give "sub" a more precise type, which rules out any of
the argument pairs for which the behavior of "sub" is undefined.