RE: type safety

This discussion on type safety has been interesting, but seems to founder 
occasionally on what exactly the definitions are for the terms being 
bandied about.  I'm in the midst of writing a book on types and semantics 
for object-oriented languages.  While writing it, I found remarkably little 
published on the definitions of such terms as "type-safe" and 
"strongly-typed".  In the hopes of both contributing to the discussion and 
(hopefully) getting some feedback on what I wrote, I've attached 
two excerpts from my manuscript.  I am presenting them in the reverse order 
that they actually appear in the manuscript because the later one is both 
shorter and more relevant.  I would be interested in comments on both.  
The reference to Cardelli is his chapter on Type Systems in the Handbook of
Computer Science and Engineering (Matthias also referred to this article in 
one of his posts).  \SOOL refers to a simple OO language described in the 


>From Chapter 12 of my book manuscript:

Cardelli \cite{CardelliHBCS} distinguishes between what he calls 
\emph{trapped} and \emph{untrapped errors}.  Trapped errors cause a 
computation to stop immediately, while untrapped errors may allow the 
computation to continue (at least for a while).  An example of an 
untrapped error might be accessing data beyond the end of an array in 
a language like C. Cardelli argues that a \emph{safe} language is one 
that does not allow any untrapped errors to occur at run-time.

In a given language, a subset of the errors may be designated as 
forbidden errors.  The forbidden errors should include all untrapped 
errors as well as a subset of trapped errors.  A language where none 
of the legal programs can generate forbidden errors is said to be 
\emph{strongly checked}.  

For \SOOL, as with most typed programming languages, the forbidden 
errors will include all run-time type errors.  It is difficult to 
characterize exactly what type errors are without listing them all 
explicitly.  However, a reasonable definition of a type error is an 
attempt to perform an operation that makes no sense based on the types 
(not values) of the arguments.  

For example, if \texttt{f} is a function taking integers to integers, 
then it makes no sense to apply \texttt{f} to an object of type 
\texttt{PointType}.  Similarly it makes no sense to attempt to apply 
an object (as though it were a function) to an integer.  The type 
error we are most concerned with in object-oriented programming 
languages is to send a message to an object which does not have a 
method corresponding to the message.

Examples of non-type errors include dividing an integer by zero (since 
both operands are integers, the division makes sense based on the 
types).  Similarly sending a message to a \texttt{nil} object is not a type 
error as long as the static type of the \texttt{nil} object includes 
the message name.  Accessing data beyond the end of an array is also 
not a type error (though it hopefully is a forbidden error in the 
language).  Finally, a non-terminating program is generally not the 
result of a type error.

Statically type-safe languages ensure that programs which pass the 
type-checker will not generate type errors at run-time (though other 
forbidden errors may be detected and handled at run-time).  Programs 
that do not pass the type-checker are not considered legal programs.  
Semantics are generally only provided for legal programs of the 

>From the introductory chapter:

Every value generated in a program is associated with a type.  In a 
strongly typed language, the language implementation is required to 
provide a correct type checker that ensures that no type errors will 
occur at run time.  For example, it must 
check the types of operands in order to ensure that nonsensical 
operations, like dividing the integer 5 by the string ``hello'', are 
not performed.  Strongly typed languages may either be dynamically or 
statically type checked.  Dynamic type-checking normally occurs 
during program execution, while static type-checking normally occurs 
at compile time.  Other type-related checks may also take place at program 

In a dynamically typed language like LISP or Scheme, many 
operations are type-checked just before they are performed.  Thus the 
code for a plus operation may have to check the type of its operands 
just before the addition is performed.  If both operands 
are integers, then an integer addition is performed.  If both operands 
are floating point numbers or one is floating point and the other is an 
integer, then a floating point addition is performed.  However, if one 
operand is a string and the other is a floating point number then 
execution is terminated with an error message.  In some languages, an 
exception may be raised, which may either be handled by the program before 
resuming normal execution or, if there is no handler or no handler 
can successfully execute, the program terminates.

In a statically typed language, every expression of the language is
assigned a type at compile time.  If the type system can ensure that the 
value of each expression has a type compatible with the statically 
assigned type of the expression,
then type checking of most operations can be moved to compile time.  

Dynamically typed programming languages can be more expressive and 
flexible than statically typed languages, because the type checking 
is postponed until run-time.  It is undecidable in general to determine 
statically for an arbitrary program whether 
a type error will occur at run time.\footnote{We leave it as an 
exercise for the more sophisticated reader to show this problem can 
be reduced to the halting problem.  Hint:  Have a type error result 
only if a program input as data halts.}  As a result, static type 
checkers will rule out some programs as potentially unsafe
that would actually execute without a type error.  

While the exclusion of safe programs would seem to be a major problem
with static type checking, there are many advantages to having a
statically type-checked language.  These include:
    \item providing earlier, and usually more accurate, information on
	programmer errors,

    \item providing documentation on the interfaces of components (\eg,
    procedures, functions, and packages or modules),

    \item eliminating the need for run-time type checks that can slow
	program execution and increase program size, and
    \item providing extra information that can be used in compiler
As a result most modern languages have static type systems.

Procedural languages like Pascal \cite{Pascal}, Clu \cite{Liskclu},
Modula-2 \cite{Modula2}, and Ada 83 \cite{DoD}, and functional languages like 
ML \cite{HMM86} and Haskell \cite{Haskell}
have reasonably safe static typing systems.  While some 
of these languages have a few minor
holes in the type system (\eg, variant records in Pascal), languages
like ML, Haskell, CLU, and Ada provide fairly secure type systems.

	Kim Bruce