Why type checking?

Every value generated in a program is associated with a type. In a strongly typed language, the language implementation is required to check the types of operands in order to ensure that nonsensical operations, like dividing the integer 5 by the string ``hello'', are not performed. In a dynamically typed language most operations are type-checked just before they are performed. 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 type of the expression, then type checking of most operations can be moved to compile time.

There are many advantages to having a statically type-checked language. These include providing earlier (and usually more accurate) information on programmer errors, providing documentation on the interfaces of components (e.g., procedures, functions, and packages or modules), eliminating the need for run-time type checks, which can slow program execution, and providing extra information that can be used in compiler optimizations. One possible disadvantage of static typing is that because static type checkers are necessarily conservative, a static type checker for a programming language may disallow a program that would in fact execute without error. Thus statically typed programming languages may be less expressive than dynamically typed languages.

Procedural languages like Pascal [Wir71], CLU [L+81], Modula-2 [Wir85], and Ada 83 [US 80], and functional languages like ML [HMM86] and Haskell [HJW92] have reasonably safe static typing systems. While some of these languages have a few minor holes in the type system (e.g., variant records in Pascal), languages like CLU and Ada provide fairly secure type systems. Moreover, support for polymorphism has been very helpful in increasing the expressiveness in statically typed imperative and functional programming languages like CLU, Ada, ML, and Haskell.

Unfortunately the situation for static type checking in object-oriented languages is not as good. The following is a list of some properties of type-checking systems of some of the more popular object-oriented languages (or the object-oriented portions of hybrid languages).

• Some show little or no regard for static typing (e.g., Smalltalk [GR83]).
• Some have relatively inflexible static type systems, which require type casts to overcome deficiencies of the type system. These type casts may be unchecked, as in C++ [Str86] and Object Pascal [Tes85], or checked at run-time, as in Java [AG96].
• Some provide mechanisms like ``typecase'' statements to allow the programmer to instruct the system to check for more refined types than can be determined by the type system (e.g., Modula-3 [CDG+88], Simula-67 [BDMN73], and Beta [KMMPN87]).
• Some of these also allow ``reverse'' assignments from superclasses to subclasses, which require run-time checks (e.g., Beta, Eiffel [Mey92]).
• Some require that parameters of methods overridden in subclasses have exactly the same types as in the superclasses (e.g., C++, Java, Object Pascal, and Modula-3), resulting in more inflexibility than would be desirable, while others allow too much flexibility in changing the types of parameters or instance variables, requiring extra run-time or link-time checks to catch the remaining type errors (e.g., Eiffel and Beta).

All of these languages require programmers to program around deficiencies of the type system or allow run-time type errors to occur. While features like typecase statements or run-time checked reverse assignments may occasionally be necessary to handle difficult problems with heterogeneous data structures, we would prefer to have type systems which allow us to program as naturally as possible, while catching all type errors. As we shall see later, many problems arise because of the conflation of type with class and with the mismatch of the inheritance hierarchy with subtyping. Whatever the cause, there appears to be a lot of room for improvement in moving toward a combination of better security and greater expressiveness in the type systems.