[Prev][Next][Index][Thread]
Re: type safety
Matthias,
I agree with you on one of your ongoing points: that type systems
do not prevent all of the safety checks that may need to be done
at runtime. The examples you give (division-by-zero,
out-of-bounds array access) are good evidence. One can certainly
imagine fancier type systems preventing more of these checks, but
the uncomputability argument means that static type systems cannot
rule out all such errors.
I don't want to argue the benefits/drawbacks of static and dynamic
type systems from the safety perspective, because it seems like an
unproductive argument.
All I want to make a simple point. Types are not just about
safety---despite the fact that the main theorem most people
(including me) prove about type systems is a safety theorem.
Types are also there to enforce abstraction.
I should have included more examples than just compilers, because
nothing in my position depends on them. For instance, types in
many languages allow a programmer to define his or her own data
abstractions. The static type system protects data from
accidental misuse. Just as in the compiler example, one can have
different types that happen to have the same representation. For
instance, one can have stacks represented as lists and sets
represented as lists, and the type system will ensure that the
"union" operation is not applied to stacks.
You might call this a safety property, but it goes deeper. It is
not just that certain errors will not happen, but that the
implementation of the abstract type can be changed in the future
without consequences. That property is the "representation
independence" theorem. A programmer can change the representation
type, and the implementation of the operations, and as long as
there is some relationship to the original implementation, the
results of the program will not change.
Types can appear in other places as well. Some of the checks done
by the JVM might be called static type checks; and one can
certainly imagine linkers that do type checking as well to
maintain invariants.
By the way, I see no reason why "soft typing" and other similar
analyses go against this philosophy. They give the implementor
certain freedom over choosing representations for types. It seems
to me to be a slippery slope to try to distinguish "analyses" from
"rule-based type systems".
The bottom line: a system is a type system if it allows one to
enforce abstractions. I'm open to examples, but I don't know of
an example of a purely dynamic "type system" that allows
representation independence-like properties.
Best,
-Jon