1 INTRODUCTION This is the first article in a regular series on object-oriented type theory, aimed specifically at non-theoreticians. The object-oriented notion of classification has for long been a fascinating issue for type theory, chiefly because no other programming paradigm has so sought to establish systematic sets of relationships between all of its types. Over the series, we shall seek to find answers to questions such as: What is the difference between a type and a class? What do we mean by the the notion of plug-in compatibility? What is the difference between subtyping and subclassing? Can we explain inheritance, method combination and template instantiation? Along the way, we shall survey a number of different historical approaches, such as subtyping, F-bounds, matching and state machines and seek to show how these models explain the differences in the behaviour of popular object-oriented languages such as Java, C++, Smalltalk and Eiffel. The series is titled "The Theory of Classification", because we believe that all of these concepts can be united in a single theoretical model, demonstrating that the object-oriented notion of class is a first-class mathematical concept! In this introductory article, we first look at some motivational issues, such as the need for plug-in compatible components and the different ways in which compatibility can be judged. Reasons for studying object-oriented type theory include the desire to explain the different features of object-oriented languages in a consistent way. This leads into a discussion of what we really mean by a type, ranging from the concrete to the abstract views.
The eventual economic success of the object-oriented and component-based software industry will depend on the ability to mix and match parts selected from different suppliers [1]. In this, the notion of component compatibility is a paramount concern: - the
*client*(component user) has to make certain assumptions about the way a component behaves, in order to use it;
- the
*supplier*(component provider) will want to build something which at least satisfies these expectations;
But how can we ensure that the two viewpoints are compatible? Traditionally the notion of *syntactic*compatibility - the component provides all the expected operations (type names, function signatures, interfaces);
*semantic*compatibility - the component's operations all behave in the expected way (state semantics, logical axioms, proofs);
and these are both important, although most work published as "type theory" has concentrated on the first aspect, whereas the latter aspect comes under the heading of "semantics" or "model checking". There are many spectacular examples of failure due to type-related software design faults, such as the Mars Climate Orbiter crash and the Ariane-5 launch disaster. These recent high-profile cases illustrate two different kinds of incompatibility.
How strictly must a component match the interface into which it is plugged? In Pascal, a strongly-typed language, a variable can only receive a value of exactly the same type, a property known as Furthermore, all object-oriented languages are A simple approach to interface satisfaction is We shall call the more complex, polymorphic approach To summarise so far, there are three different degrees of sophistication when judging the type compatibility of a component with respect to the expectations of an interface: - correspondence: the component is identical in type and its behaviour exactly matches the expectations made of it when calls are made through the interface;
- subtyping: the component is a more specific type, but behaves exactly like the more general expectations when calls are made through the interface;
- subclassing: the component is a more specific type and behaves in ways that exceed the more general expectations when calls are made through the interface.
Certain object-oriented languages like Java and C++ practise a halfway-house approach, which is
How can we explain the behaviour of languages such as Smalltalk, C++, Eiffel and Java in a consistent framework? Our goal is to find a
There are various definitions of type, with increasing formal usefulness. Some approaches are quite concrete, for example a programmer sometimes thinks of a type as a
An afficionado of formal methods (such as Z [8], or VDM) likes to think of types as This is called the Concrete approaches have their limits [10], for example, how would you specify an
A type theorist typically thinks of a type as a set of in which can be read as "let there be an uninterpreted set ord", such that the following operations accept and return elements from this (as yet undefined) set. Ordinal is then defined as the type providing first and succ; and we don't care about the representation of ord. This approach is variously called syntactic, since it is based on type signatures, or existential, since it uses to reveal the existence of a representation, but refuses to qualify ord any further. Although syntactic types reach the desired degree of abstraction away from concrete models, they are not yet precise. Consider that the following faulty expressions are still possible: succ('b') = first() = 'a' - an undesired possibility; succ(1) = 1 - another undesired possibility; This is because the signatures alone fail to capture the intended meaning of functions.
A mathematician considers a type as a set of signatures and constraining axioms. The type Ordinal is fully characterised by: This form of definition is known as an algebra. Formally, an algebra consists of: a sort (that is, an uninterpreted set, ord, acting as a placeholder for the type); and a set of functions defined on the sort (first, succ), whose meaning is given by axioms. The two axioms (1) and (2), plus the logical rule of induction, are sufficient to make Ordinal behave in exactly the desired way. But how do the axioms work? Let us arbitrarily label: x = first(). - From (1), succ(x) first(), so we know succ(x) is distinct from x; let us choose another arbitrary label: y = succ(x).
- From (2) succ(y) y; from (1) succ(y) * x, so we know succ(y) is distinct from x and y; let us therefore label: z = succ(y) = succ(succ(x)).
- From (2) succ(z) z; from (1) succ(z) x; but could succ(z) = y? Although there is no ground axiom that instantly forbids this, induction rules it out, because:
by substitution of y and z, we get: succ(succ(succ(x))) = succ(x) by unwinding succ, we get: succ(succ(x)) = x, which is false by (1), so succ(z) is also distinct; and so on...
Once the algebra is defined, we can disregard the sort, which is no longer needed, since every element of the type can now be expressed in a purely syntactic way: first(); succ(first()); succ(succ(first())); ... The algebraic definition of Ordinal says exactly enough and no more [11]; it is both more abstract than a concrete type - it is not tied to any particular set representation - and is more precise - it is inhabited exactly by a monotonically-ordered sequence of abstract objects.
We are motivated to study object-oriented type theory out of a concern to understand better the notion of syntactic and semantic type compatibility. Compatibility may be judged according to varying degrees of strictness, which each have different consequences. Likewise, different object-oriented languages seem to treat substitutability in different ways. As a preamble to developing a formal model in which languages like Smalltalk, C++, Eiffel and Java can be analysed and compared, increasingly abstract definitions of type were presented. The next article in this series builds on the foundation laid here and deals with models of objects, methods and message-passing.
[1] B. J. Cox, [2] Mars Climate Orbiter Official Website, http://mars.jpl.nasa.gov/msp98/orbiter/, September 1999. [3] J. L. Lions, [4] J. C. Reynolds, [5] L. Cardelli and P. Wegner, [6] B. Meyer, [7] W. Harris, [8] J. M. Spivey, [9] P. Martin-Löf, [10] J. H. Morris, [11] K. Futatsugi, J. Goguen, J.-P. Jouannaud and J. Messeguer,
Cite this column as follows: Anthony J. H. Simons: "The Theory of Classification, Part 1: Perspectives on Type Compatibility", in |