Typing in object-oriented languages:
Achieving expressiveness and safety

Kim B. Bruce

Williams College
October 28, 1998

Abstract:

While simple static-typing disciplines exist for object-oriented languages like C++, Java, and Object Pascal, they are often so inflexible that programmers are forced to use type casts to get around the restrictions. At the other extreme are languages like Beta and Eiffel, which allow more freedom, but require run-time or link-time checking to pick up the type errors that their type systems are unable to detect at compile time.

This paper presents a collection of sample programs which illustrate problems with existing type systems, and suggests ways of improving the expressiveness of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing ``MyType'', ``matching'', and ``match-bounded polymorphism'' into these type systems.

We also suggest a way of simplifying the resulting type system by replacing subtyping by a type system with a new type construct based on matching. Both systems provide for binary methods, which are often difficult to support properly in statically-typed languages.

The intent is to explain why the problems are interesting via the series of sample programs, rather than getting bogged down with pages of type-checking rules and formal proofs. The technical details (including proofs of type safety) are available elsewhere.