Report Number: CS-TN-96-31
Institution: Stanford University, Department of Computer Science
Title: Classes = Objects + Data Abstraction
Author: Fisher, Kathleen
Author: Mitchell, John C.
Date: January 1996
Abstract: We describe a type-theoretic foundation for object systems that include ``interface types'' and ``implementation types.'' Our approach begins with a basic object calculus that provides a notion of object, method lookup, and object extension (an object-based form of inheritance). In this calculus, the type of an object gives its interface, as a set of methods and their types, but does not imply any implementation properties. We extend this object calculus with a higher-order form of data abstraction that allows us to declare supertypes of an abstract type and a list of methods guaranteed not to be present. This results in a flexible framework for studying and improving practical programming languages where the type of an object gives certain implementation guarantees, such as would be needed to statically determine the offset of a method or safely implement binary operations without exposing the internal representation of objects. We prove type soundness for the entire language using operational semantics and an analysis of typing derivations. One insight that is an immediate consequences of our analysis is a principled, type-theoretic explanation (for the first time, as far as we know) of the link between subtyping and inheritance in C++, Eiffel and related languages.
http://i.stanford.edu/pub/cstr/reports/cs/tn/96/31/CS-TN-96-31.pdf