[Prev][Next][Index][Thread]
RE: type safety
Kim has a point: part of the confusion here is over the definitions of the
terms, plus some continuing confusion about how various concepts fit
together.
First point: "safety" is a *per-language* property. Each language comes
with its own notion of safety. ML is ML-safe; C is C-safe; etc. I'm not
being facetious; I think this is the core of the confusion.
Safety is an internal consistency check on the formal definition of a
language. In a sense it is not interesting that a language is safe,
precisely because if it weren't, we'd change the language to make sure it
is! I regard safety as a tool for the language designer, rather than a
criterion with which we can compare languages.
To be more precise, here is what I have in mind. First, you fix a set P of
(well-formed) programs. This can be done by a variety of means, but I will
not specify these here for the sake of generality. Second, having fixed the
set P of programs, you define a transition system over P, consisting of two
things: (1) a predicate defining the terminal states of the transition
system (these are irreducible, but not all irreducible states need be
terminal), (2) a binary transition relation between programs subject to the
condition that if p is terminal, then there is no q st p transitions to q.
Having done this (ie, having defined your programming language), you can
then state what is meant by safety, and not before. To be safe (better:
coherent or well-defined) a language must satisfy two properties:
1. If p in P and p transitions to q, then q in P. Well-formedness is
preserved.
2. If p in P, then either terminal(p) or there exists q such that p
transitions to q.
If your language does not satisfy both of these properties, then it is not
safe. For emphasis, we should really say "not safe for the given
definitions of program and transition". If safety doesn't hold, we can do
one of two things:
1. Change P to some other P' for which safety holds.
2. Change the transition system (including terminal property) to make safety
hold.
Option (2) is deceptive since the set of programs doesn't change, only their
interpretation. This invites misunderstanding. To keep sane remember that
the programming language is defined by BOTH the set of programs AND the
transition relation.
Examples:
1. Famously, the ML core language is ML-safe. This is essentially Milner's
Theorem. Milner relied on an ad hoc denotational semantics that forced
certain values to be a designated "wrong" element of the model. Why this
led to the catchy phrase "well-typed programs cannot go wrong", experience
shows that this setup is more misleading than helpful, and few use it any
longer.
2. I claim that C is C-safe. Well, almost. The trouble is that I've never
seen a formal definition of C in which we precisely specify both the set of
program and the operational semantics. But if we did, it would be safe (or
would be made to be safe). Incidentally, C-safe programs could still incur
bus errors! Why? Because Unix misimplements the operational semantics of
C, which is fundamentally a mapping from memories to memories. It is
perfectly sensible for a C program to make reference to an arbitrary memory
address; the notion of bus error that sometimes arises in such cases is
Unix's fault, not C's. BTW, it would be extremely nasty to write down a
formal definition of C, at least if you admit things like casting a memory
address as a function pointer --- this forces the semantics to define
programs as data values in a way that's sure not to be portable (or in a way
that people would refuse to implement).
3. If you add, say, integer division to the ML core language with type int *
int -> int, then the resulting language is NOT (ML+division)-safe, for the
obvious reason that 1 div 0 is neither a value nor can it make a transition.
There are two approaches to fixing this: change P or change the transition
system. Changing P involves imposing more constraints on well-formed
programs to ensure that this case cannot arise. More on this below.
Changing the transition system involves designating division by zero as a
checked error, introducing error as a valid outcome of program execution
(ie, a terminal state), and recovering safety by defining 1 div 0 to
transition to error.
4. Scheme is a Scheme-safe language, for obvious reasons, given what I've
said above.
As Greg pointed out there are many ways to specify the set P. Some
languages, such as Scheme, require very, very little to be a valid member of
P. Others, such as ML or other "type-theoretic" languages, require
substantially more, imposing context-sensitive constraints on the formation
of programs. The reason to impose context-sensitive constraints is
precisely as Reynolds put it: to SYNTACTICALLY enforce levels of
abstraction, eg to guarantee representation independence without ANY
run-time cost. (Zero cost is better than some cost, however small.) There
is NO LOSS OF GENERALITY in imposing context-sensitive constraints, if your
language is rich enough, since you can always (selectively or grossly)
ignore them. A lot of confusion arises from misunderstanding this
fundamental (yet simple) point. Too often in these discussions people
compare Scheme to the simply typed lambda calculus, being apparently unable
to imagine any other type system, eg one that subsumes Scheme as a special
case. (A related point is the apparent inability of some writers to imagine
type inference, equating typed languages with those that require huge
amounts of type information to be explicitly and tediously maintained by the
programmer. Ousterhout comes to mind here.)
As a matter of historical context, and in answer to Phil Wadler's question,
let me mention that this notion of safety is implicit in Martin-Lof's 1976
type theory and the NuPRL type theory on which it is based. It appears
there in the concept of the canonical forms theorem, which characterizes the
forms of values of a given type, from which it follows immediately that the
language is safe (in its own internal sense). I claim that this is the
first instance of a rigorous principle of safety in a programming language,
pre-dating Milner's later notion.
Once we have a well-defined programming language in hand (ie, one satisfying
safety), we can (and only then) talk about the operational behavior of
programs. For example, we might be interested in those programs that cannot
incur division by zero. This is a property of well-formed programs over a
specific operational interpretation, which must be fixed in advance. Once
we have this, we can then introduce properties of programs, essentially
predicates over the operational semantics. Let us write x:tau |- phi prop
to indicate that phi is a property of expressions of type tau. For example,
we might consider the property
f:int->int |- (for all x:int f(x) does not evaluate to error) prop
Such a property may or may not hold. We write phi(e) true when phi is true
of e. Typically phi is not decidable, given e, but in some cases it might
be; we make no assumptions about whether or not this is the case.
What is a suitable language of properties? This is the subject of ongoing
research. We might consider equivalences between expressions, definedness
(purity) assertions, or modal assertions about the underlying transition
system, or complexity assertions, to name a few. One class of assertions
that arises very naturally are those that are induced by the type system.
This is the notion of logical relations. Essentially each type determines a
"canonical" property of values of that type, which turns out to be true of
all values of that type. The fundamental theory of logical relations tells
us that for every type tau,
forall x:tau phi_tau(x) true
where phi_tau is the canonically induced property of values of type tau.
This is essentially the safety theorem expressed as a property. Logical
relations become much more interesting in the presence of variable types;
they form the basis for a rigorous treatment of representation independence
for ADT's via the notion of parametricity.
Lots of other properties are of interest. For example, in ML with errors,
we can consider the property of functions that do not incur an error when
applied. Such properties (sometimes, rather misleadingly, called a "soft
types" or a "refinement types") are interesting and important, but they are
only rarely part of the fundamental type system of the language. However,
they could be made so, for example, by adding comprehension types:
{ x:tau | phi(x) } type
if x:tau |- phi(x) prop
e : {x:tau|phi(x)}
if phi(e) true
phi(e) true
if e:{x:tau|phi(x)}
Once we have props around we can exploit them to express sharper
requirements on well-formedness of programs. Clearly to be well-formed in
this sense requires mathematical proof; quite often we don't go that far,
but we can (and some systems, such as NuPRL, do).
But we need not go this far! We can simply content ourselves with
properties, and checking whether they are true or not. The only problem is
that with this approach there is no means of attaching properties --- or
their proofs --- to programs. Current research is concerned with how to do
just that, without passing to a full-blown dependent type system.
My point here is to establish a firm framework for sensible discussion. Too
much of this discussion revolves around ill-understood or ill-defined
concepts. If we can all agree first on the framework, then it will be quite
easy to situate various ideas within it.
Bob Harper