Anthony J H Simons, MA PhD

Senior Lecturer in Computer Science

You are here: Simons Home / Research / Projects / Theory of Classification /
Department of Computer Science
Verification and Testing Research Group
The Brunel Object-Oriented Language
The Poppy Object-Oriented Language
The Theory of Classification

The Theory of Classification

Object-oriented programming languages were originally developed in advance of any formal theory of classification and, as a result, their treatment of class was muddled and ill-founded. Strongly-typed languages assumed that the notion of class was equated with type, and behavioural compatibility could be described using a terminology of types and subtyping, which strictly did not apply. The type systems of languages affected by such misunderstandings were sometimes incorrect. Other languages assumed that objects have class and type independently, relegating the notion of class to a mere implementation construct.

To counter this confusion, a mathematical theory of classification was developed, which encompassed other approaches to type abstraction, such as "type constructors", "generic parameters", "classes", "inheritance" and "polymorphism". The theory extended earlier work on F-bounded polymorphism by providing second- and higher-order typed record combination for objects modelled as records of functions. The theory captures notions such as single, multiple and mixin inheritance and unifies the treatment of generic polymorphism with inheritance-based polymorphism. Object-oriented languages such as Smalltalk, C++, Eiffel and Java may be explained within the theory, which also shows how the syntactic treatment of type polymorphism may be simplified in future object-oriented languages.

Project History

This project grew out of a personal dissatisfaction with the various ad-hoc typing mechanisms used to express polymorphism in object-oriented programming languages. Inspired by Cook's account of how a strongly-typed object-oriented language violated mathematical subtyping, by permitting covariant specialisation of method argument types [1], work started on an object-oriented language, which was to support strict subtyping (Simons, 1991) and whose subtyping rules also regulated the permissible refinements of pre- and postconditions (Simons, 1994a).

Subsequently, the type system of this language, Brunel, was completely redesigned to accommodate Cook's new theory of F-bounded polymorphism, which treated a class as a second-order construct in the function-bounded polymorphic λ-calculus [2], [3]. From this, an initial approach was developed to unify the object-oriented notion of inclusion polymorphism with more traditional notions of parametric polymorphism and type constructors (Simons and Cowling, 1992). The unified theory of classification was summarised in (Simons, 1996a) and was presented as tutorials at ECOOP and OOPSLA (Simons, 1993a, 1993b, 1994b), in which the consequences of adopting an F-bounded type system were explored. A class is a function-bounded second-order construct in the λ-calculus, whereas an object type is the least fixed point, a first-order construct. Different parametric type checking rules apply, which permit the covariant specialisation of method argument types, as object-oriented languages intuitively seem to require.

Distinguishing the notion of class from type

The unified theory of classification was the subject of the PhD thesis (Simons, 1995a), which also described the Brunel 2.0 language as an exemplar of the new type system. This presented a unified treatment of inheritance and genericity (templates), showing how the interactions of different kinds of extension and specialisation by inheritance and by parametric specialisation and substitution are confluent. This eventually extended Cook's model from second-order to higher-order, but could be approximated by dependent second-order types some of the time, such as the treatment of mixins in (Simons, 1995b). The impact of the theory upon another object-oriented language, Eiffel, was described in (Simons, 1995c, 1995d). This provided an alternative second-order, F-bounded solution to the type-failure problem, which Cook had addressed earlier using first-order subtyping [1]. The revised solution permitted covariant method argument specialisation, as found in Eiffel, but also replaced three different syntactic mechanisms for expressing polymorphism (conformance, anchored types, constrained genericity) by a single mechanism. The popular impact of the theory of classification upon language terminology and design notation was discussed in (Simons, 1996b).

Most recently, the Theory of Classification has reached a much wider audience, through the publication of an invited series of articles in the Journal of Object Technology. This is a popular monograph, serialised in 20 parts (Simons, 2002 - 2005). This material has over 100 citations and is collated on a number of specialist websites, such as the community weblog for programming language research, Lambda the Ultimate. The material has formed the basis for a number of courses on object-oriented type theory at the Universities of Berne (Switzerland), Sheffield (UK) and others.

Journal of Object Technology

Related Publications

The Theory of Classification is published as a popular monograph, serialised in 20 parts from 2002-2005 in the Journal of Object Technology. Links to the published articles are given below. In Spring 2008, the journal changed the location of these articles. The links have been updated.

Other related publications described in the history above are given below:

Regent Court, 211 Portobello Street, Sheffield S1 4DP, United Kingdom