Authors: Bruce, Kim B.
Pages: 384
Publisher: MIT
ISBN13: 9780262025232
I wrote this book to provide a description of the foundations of statically
typed class-based object-oriented programming languages for those inter-
ested in learning about this area. An important goal is to explain how the
different components of these languages interact, and how this results in
the kind of type systems that are used in popular object-oriented languages.
We will see that an understanding of the theoretical foundations of object-
oriented languages can lead to the design of more expressive and flexible
type systems that assist programmers in writing correct programs.
Programmers used to untyped or dynamically typed languages often com-
plain about being straitjacketed by the restrictive type systems of object-
oriented languages. In fact many existing statically typed object-oriented
languages have very restrictive type systems that almost literally force pro-
grammers to use casts or other mechanisms to escape from the static type
system. In this work we aim to meet the needs of a programmer who wants
a more expressive type system. Thus another goal of this text is to promote
richer type systems that reduce the need for bypassing the type checker.
Because of the semantic complexity of the features of object-oriented lan-
guages, particularly subtyping and inheritance, it is difficult to design a static type systemthat is simultaneously safe and flexible. To be sure that there are no holes in the type system we need to prove that the type system is safe
(essentially that no type errors can occur at run time), but we cannot do that
without a description of the meaning of programs. Thus this book contains
careful formal descriptions of the syntax, type system, and semantics of sev-
eral progressively more complex object-oriented programming languages.
With these definitions, it is possible to prove type safety.