The Theory of Classification Part 20: Modular
Checking of Classtypes
Anthony J H Simons, Department of Computer Science, University of Sheffield,
UK
|
 |
COLUMN
PDF Version |
1 INTRODUCTION
This is the final article in an informal series on the Theory
of Classification,
which has considered the theoretical notions of type and class in
object-oriented languages. The series began by constructing models
of objects, types, classes and inheritance, then branched out into
interesting areas such as mixins, multiple inheritance and generic
classes. The core of our argument has been that the notions of class and type are
distinct, but both can be described formally in the  -calculus. Strongly-typed
object-oriented programming languages
are largely based on the idea that “a class is a type” and “subclassing
is subtyping” [1]. In earlier articles, we demonstrated why
this is not really satisfactory as a formal model of classes and
classification. A type system based on first-order types and subtyping:
- fails to capture natural relationships between recursive
types (whose methods accept or return values of the same type as
themselves), since
recursive types can have no proper subtypes [2];
- loses type information when methods are inherited [2],
requiring the use of type downcasting everywhere to recover
the most specific type of the object returned by a general method,
which is tantamount to
breaking the type-system;
- conflicts with the notion of type classes adopted
elsewhere in functional programming languages like Haskell, which
use type parameters to express
this notion [3].
Instead, we have argued that a class is a family
of related types,
which can only be expressed in a second-order type system with polymorphism
[4]. Classical polymorphism is represented using type parameters that
range over many different actual types, but object-oriented programming
requires a kind of polymorphism where type parameters receive only
certain related types that satisfy a particular interface description.
Mathematically, this is constructed by placing constraints on type
parameters, called function bounds, or F-bounds,
which have form:  <:
F[], where F is a type
function, describing the shape of the interface that the type is
expected to satisfy [5]. However, while this gives
a much more satisfying account of classes and classification, very
few programming languages have ventured into this new and exciting
territory. In this final article, we try to understand why this is
so; and what practical problems remain to be solved in the modular
checking of class-types.
2 TRADING MODULARITY AND EXPRESSIVENESS
A first-order type system has two things to commend it. Firstly,
it is quite simple to implement a type-checker that can check types
for exact correspondence, or for subtype compatibility with a given
type. The type of the source object can be compared with that of
the target variable to see if the former can be converted up to the
latter, using subtyping rules like those we discussed in [1]. Secondly,
code that has been checked once need never be checked again, or recompiled
in new contexts. This is because the type system can never reveal
more specific information about an object that is passed into a more
general variable (which we have called the “type loss problem”),
so the code need only be checked once over the most general type
that it can accept. This, more than any other reason, is why object-oriented
languages have been slow to take up the new insights into the nature
of classes and classification: the desire to have modular and incremental compilation. Without this, it would not be possible to build industrial-scale
systems.
In the last two articles, we showed that full support for the notion
of classes and subclassing requires a distinction to be drawn between
simple, monomorphic types and polymorphic classes, the latter formally
expressed using type parameters [6]. However, this means that type
checking rules are more complicated. The compiler has to keep track
of sets of type parameters, one for each variable with a “class-type”,
and has to know how to substitute one parameter for another when values
are passed, and also check that the various constraints on the parameters
will allow the given substitutions [3].
Now, different type substitutions may happen upon different occasions.
For example, consider a polymorphic method for moving graphical shapes
on a screen, that accepts Integer coordinates and returns the moved
object:
This method is defined for a polymorphic class of Shapes, expressed
by ]
in the style described in earlier articles [2, 4]. Below, we assume
that Square and Circle are exact types that
satisfy
this F-bound constraint. Now, if move is legally invoked on
different actual shapes on different occasions, say on a Square and
a Circle,
this will cause the two different type substitutions {Square/} and
{Circle/}, yielding two differently-typed versions of the
move method. These variants will have have the exact types:
for the duration of the binding of the (polymorphic)
argument to the (exactly-typed) objects. Does this mean that we must
compile two different versions of the source-code for move?
Well, if Circle and Square were passed by value, then we should need
multiple compilations of the source to handle the different physical
layout of each type – this would be analogous to the template
mechanism in C++, in which multiple copies of the template code are
compiled, one copy for each distinct type-instantiation. However, it
is more likely that the objects will be passed by reference and both
will share the same physical layout (in the low-order bytes) for storing
information about their screen location. This case therefore has more
similarities with Java 1.5’s treatment of type parameters. They
are used in the typechecker to eliminate the need for explicit type
downcasting, but are erased later in the virtual machine, in which
objects are treated in the same way as in the usual subtyping approach.
So, having flexible typing for move does not necessarily require multiple
compilations of this method.
Nonetheless, the polymorphic typing situation is quite different
from the kind of typing that is possible in a first-order type system.
In
the latter, the result of move can only ever have the general type
Shape, which is typically not useful, especially if we want to do something
else with the moved object (for which we would first have to perform
a type downcast). But, in the second-order type system, we recover
the exact type of the moved object straight away. This is good, from
the point of view of expressiveness.
Now, consider the context in which move was called. What does this
context expect the result-type to be? It knows the result must be some
type ], but, on different occasions, it receives
back objects of the more specific types Square and Circle. It is possible
to optimise further method invocations on these results, on the basis
of this type analysis. For example, imagine that the Shape class declares
an abstract method area(), which has distinct implementations in all
subclasses. The method area() may be statically bound, if we can tell
in advance that the target is definitely a Square or a Circle, rather
than some unknown kind of Shape, for which we would have to insert
a dynamically-bound call, to detect the exact type at run-time. However,
using the more expressive polymorphic type system, we can propagate
exact type information back into the calling context and choose to
bind the area() method statically. The cost of this is that we must
compile multiple versions of the context code.
Simons et al. first analysed these kinds of parametric issues as
part of a wider optimisation strategy for object-oriented compilers,
using
the experimental language Brunel as an exemplar for the techniques
[7]. They discovered that a fully parametric type system gives you
the choice of using more or less of the exact type information available,
to tailor the optimisation of bindings. The early binding algorithm
described in [7] bears some similarities to Chambers and Ungar’s
notion of pre-emptive type analysis in the untyped language Self [8].
However, the trade-off is that the more type information you use, the
more copies of the object-code you generate. In Brunel, a global compilation
approach was adopted, in which a full type analysis of the whole program
was performed and compiler switches could be set to control the amount
of early binding and code duplication.
The early binding approach does not transfer over to a modular compilation
strategy. When compiling modules incrementally, only partial type information
is available. For example, we must compile the methods of the Shape class, without any knowledge that it will eventually have two subclasses
Circle and Square, which we previously assumed were the “leaves” in
the class hierarchy, becoming the exact types of objects used in the
program. Obviously, the compiler could not know in advance whether
these are in fact leaf-nodes, or whether they too might eventually
be specialised further. The best that can be done is to insert a dynamically-bound
call for abstract methods like area(). No further optimisation can
be performed. However, the parametric type information can be retained
and used to avoid type downcasting on the result of move().
3 A UNIFICATION APPROACH TO PARAMETRIC TYPING
Java 1.5 is introducing a form of parametric type analysis that captures
an aspect of the strategy we describe above. However, parameters
will be used only for certain generic classes, like those in the
Java Collections framework, and will only characterise the element-types
of these collections. In our view, this same approach could be used
to characterise all class-types, in the manner described in [3].
All variables marked with a “class-type” are polymorphic
and so should be treated in a parametric way. The parametric type
information could be used everywhere in the type-checker to obtain
more exact type information, but erased in the runtime model. This
would allow code modules (classes, in Java) to be incrementally compiled,
provided that most calls were bound dynamically, as is usual in Java.
But it would also allow some optimisations and static binding of
methods for simple leaf-classes, like Integer and Boolean, for which
the compiler could be told that no further specialisations were intended.
(In fact, the Java simple types int, float, etc. could be merged
with the class-types in a single-rooted class hierarchy).
The most significant challenge to the development of proper, parametric
type-checkers is the problem of unifying different polymorphic types.
This happens whenever one polymorphic variable is passed as an argument
or result to another method, where the formal and actual types of
the variables may be distinct. However, there exists at least one programming
language, Prolog, which already has a similar algorithm at the heart
of its interpreter. This is the most general unifier (MGU) algorithm,
which calculates the most general term that can result from the unification
of two other terms.
For those unfamiliar with Prolog, this is a language in which the
programmer constructs logical expressions, in a declarative style,
and program
execution is then analogous to solving the simultaneous equation
expressed by all the terms. Terms are structured as predicates,
which may contain
grounded values (written in lowercase) or variables (written capitalised).
So, the following two terms may exist:
and it is possible to see that these terms may
be unified, yielding the MGU:
In this unification, the variable Loved in the
left-hand term receives the value mary from the right-hand term; and
the variable Lover in the right-hand term receives the value john from
the left-hand term in a symmetrical act of merging. In logic, this
is equivalent to saying: “these terms can be unified, provided
that the Lover stands for john and the Loved person stands for mary”.
The important thing to note is that both the left- and right-hand terms
contributed some of the specific values to the resulting unified term.
It is not difficult to see how this kind of substitution mirrors
the process a polymorphic type checker must go through when a polymorphic
variable receives an object of some exact type. However, this is an
even better analogy for when two polymorphic variables have their types
merged, for example when a polymorphic variable with the type <:
F[] is passed into a method,
whose formal argument has the type  <:
G[]. For the duration
of the binding, and
therefore the dual constraint must apply: <:
F[<:
G[]. In earlier articles
dealing with inheritance and multiple inheritance, we called this an intersection
type [9, 10] because the type
variable is being constrained
to accept two different, overlapping sets of types and therefore accepts
the intersection of these sets. Accordingly, we used <:
F[ ]
to denote an intersection on the parameter .
The important thing to note is that this merging of type-constraints
is even-handed: it doesn’t matter whether <:
F[<:
G[] is the more restricting
F-bound, since any type replacing must
satisfy both constraints. So, this mechanism is adequate to handle
specialisation (when a polymorphic type is replaced by a more restricted
polymorphic type [9]) and also the kind of symmetrical type-merger
that happens with multiple inheritance (when the polymorphic types
of two parent classes become unified in the child [10]). The latter
case also extends to languages with a combination of single inheritance
and multiple interface satisfaction (the -calculus model treats all
class-like and interface-like types in the same way). So, parametric
type checkers will in future need to perform unification on type variables
and compute the pool of merged constraints; but fortunately this is
no more difficult than unification in Prolog.
4 DISGUISING THE TYPE PARAMETERS
Another of the challenges to be faced is how to make genuinely polymorphic1
languages attractive to programmers. The previous article [3] reported
how such languages tend to become swamped by the proliferation of type
parameters. If each class requires its own self-type parameter, then
a class with “class-typed” polymorphic variables in its
attributes and methods needs a distinct parameter for each such variable
that could eventually be bound to a distinct type. If the classes describing
these elements also contain further “class-typed” variables
of their own, then our original class has a declaration which is already
three layers of parameters deep! We showed how the order of declaration
was significant, in that the type parameters for the inner element
classes have to be declared first, on the outside, and the dependent
type parameters standing for the outer composite classes have to
be declared within their scope (in a second-order type system). Essentially,
any polymorphic structure must expose, in its interface, all of the
different type parameters which could be bound to a different type
at some point during the execution of the program.
Various attempts have therefore been made to disguise the existence
of type parameters and the many substitution operations that must
be performed on them. Perhaps the most careful and thorough of these
treatments is Bruce’s matching. This is an alternative
to F-bounds that establishes flexible type compatibility relationships
between
class-types. Bruce and his co-workers started building type-safe
experimental object-oriented languages in the early 1990s. TOOPL
and TOOPLE were functional-style object languages (rather like the
-calculus models we have used in this series), which supported both
simple subtyping and a new treatment of the self-type using a distinguished
type variable called MyType [11]. Originally, the motivation for MyType arose from considering the same problems with subtyping in
the presence of recursive types that led Cook to devise F-bounded
quantification [5]; and Bruce’s early treatments relied on
an F-bounded explanation. However, in later work, Bruce defined complete
and consistent type rules for MyType which dispensed with explicit
F-bounds altogether. The later languages TOIL and PolyTOIL were styled
more like imperative object-oriented languages, with variable reassignment
[12].
The first advantage gained through using a distinguished MyType is
that this type variable is implicitly defined within each class-type.
The meaning of MyType is rather like the type parameter
in F-bounded
constructions like: <:
GenMyType[], but for each new class, MyType is implicitly rebound
to refer to the self-type
of the new
class-type. The implicit declaration of MyType can be seen below
in the type declaration of the abstract Comparable, which defines
abstract methods lessThan and equal; and in the type declaration
of the concrete BoxedInteger, which is essentially a wrapper for
a simple int type:
where ObjectType is the keyword introducing the
new object types (these examples are adapted from [12]). Notice how
MyType occurs freely inside both definitions, but stands in
each case for a different polymorphic type. In our approach using F-bounds,
we
would introduce two generators, which declare two self-type parameters
up-front,
and then construct F-bounds to use in type expressions:
Now, in PolyTOIL you can declare variables with
object types directly, for example, it is legal to declare myInteger
: BoxedInteger, in which all internal occurrences of MyType are
eventually resolved (in the type rules) to refer to a BoxedInteger,
recursively. The parameter MyType is replaced by the actual type of
the object receiver,
when a method is invoked upon it. In our approach using F-bounds, this
requires taking a fixpoint first:
The second innovation in Bruce’s approach
is the way in which subclass relationships can be expressed directly
between these object types, using the novel matching mechanism. You
can assert the usual subclass relationship as: BoxedInteger <# Comparable (read this as “BoxedInteger matches Comparable”), where “<#” is
the new matching operator. Bruce describes the matching relation as:
“
the same as subtyping in the absence of the MyType construct, but differs
in the presence of MyType, because MyType implicitly has different
meanings in different types.” [13].
In fact, matching behaves in a similar manner
to F-bounded inclusion, in the presence of MyType, but in a similar
manner to simple subtyping
elsewhere. In our approach, we would have to establish a second-order
pointwise subtyping relationship between the two corresponding type
generators, to ensure that the two parameters were unified before interfaces
were compared, and then that one interface were longer than the other:
Bruce’s rules simply compare the structure of object types, in
which all occurrences of MyType are considered equivalent
when determining if one type matches another. This dispenses with some
of the fiddly
detail of parameters. Matching has the same expressive power as F-bounds,
for example, note that while BoxedInteger <# Comparable,
the subtyping relationship BoxedInteger <: Comparable does
not hold, because MyType occurs as a method argument
type (in contravariant position). The type rules for inheritance ensure
that MyType evolves smoothly to represent
the self-type of inheriting classes, which dispenses with another layer
of type substitutions in the explicit approach. Finally, if the programmer
so wishes, it is also possible to declare explicit type parameters
in PolyTOIL. For example, the element-type of a SortedList may
be given as elt : T <# Comparable, to denote any
type which matches Comparable.
This is the analogue of <:
GenComparable[ in our approach. In later work, Bruce developed a version of matching
with “hash
types” that was sufficiently expressive that subtyping could
be dropped altogether [14]. This is closer to our approach, which recognises
only exact simple types, or parametric polymorphic types.
5 IMPLICIT CLASS-TYPE SUBSTITUTIONS
Perhaps the trickiest issue for future compilers, with the more thorough
kind of type analysis we have been proposing here, is to keep track
of all the subtle changes to type descriptions that happen as a
result of objects being mutually related to each other. This can lead
to
some hidden evolution in the types of expressions, of which the
programmer may not be aware! Consider a class hierarchy describing
the various
kinds of Vehicle that exist, together with the different kinds
of Location in which such vehicles are typically kept. The root concepts
could be described in Java as:
We can build a pair of mutually-referencing objects by constructing a Vehicle and a Location in either order, since their constructors set up the reciprocal
references:
Now, the intention is that these classes should be specialised
in pairs, for example, we might create Car/Garage, or Aircraft/Hangar,
or Ship/Port pairs. But what happens if the programmer only specialises
one half of this mutual relationship?
In Java, the result of enquiring loc.keeps() always has
the type Vehicle (we are suffering from the “type-loss” problem
again), but dynamically it contains an instance of Car. In a
parametric type system, we would expect to be able to recover the exact
vehicle-type.
This is because, when the Location is constructed with a value
of the exact type Car, this type is propagated into the vehicle-type
parameter of Location’s polymorphic variable myVeh, which we imagine might have the type:
This is exciting from the viewpoint of type analysis;
but notice that we have created a new, unforeseen type. We expected
eventually to specialise Vehicle and Location in step with each other,
producing Car and Garage, such that the Garage.keeps() method returns
a Car, and the Car.keptAt() method returns a Garage. Because we only
specialised one half of the mutual relationship, we created a new intermediate
type variant, a Location’ whose keeps() method returns a Car,
rather than a Vehicle. This type is neither a Location, nor a Garage,
but something in between.
Palsberg and Schwartzbach were the first to report such intermediate
types in object-oriented languages [15]. They were using a type
substitution mechanism, which has only slightly less expressive power than the
full parametric mechanism used in our approach2. They discovered that
checkers
which perform full type analysis will inevitably synthesise many
intermediate versions of types, as a result of the evolution of other
closely-related
types. The consensus nowadays is that a mutually-referring set of
types creates another enclosing formal structure, a closure, which
is specialised
as a whole, when any one of the related types is specialised. This,
then, is the challenge facing the designers of future object-oriented
compilers with smart type analysis, implicit type evolution and incremental
compilation.
6 CONCLUSIONS
Maybe in the future we will see object-oriented languages that exemplify
the Theory of Classification in full. I’d like to think that
one day, we could have a programming language that is based on a
few simple concepts, which is as type-safe as Pascal and as expressive
as Eiffel (or Algol-68, or whatever the last really good programming
language was). In my crystal ball, this language has to distinguish
the theoretical notions of class and type, to allow programmers to
understand clearly when simple, or polymorphic typing is intended.
It will relate all built-in and programmer-defined types and support
obvious, intuitive notions of classification, for example, that the
simple types Integer and Boolean are first-class members of the class/type
hierarchy and fit underneath an abstract class of Numbers, whose
abstract arithmetic-methods are appropriately specialised when they
are implemented in Integer and Real. Multiple classification will
be possible, such that both Complex numbers and Sets will be considered
PartiallyOrdered types, Complex and Integer numbers will be considered
kinds of Number, and Sets and Bags kinds of UnorderedCollection.
Interfaces will be the same thing as abstract classes.
Incremental compilation will continue to be supported and dynamic
binding will be the norm, with some static optimisations performed
on the standard
leaf-types. The syntax of these languages may start out using explicit
type parameters everywhere (such as the cutting-edge work on Haskell
type classes), but the parameters may eventually disappear
inside the compiler, maybe at the loss of a small amount of flexibility
and expressiveness.
The compiler’s ability to perform early type analysis will improve
and I expect that in future, code modules will be compiled, which retain
their type parameters, such that when the modules are linked and bound
at their call-sites, exact type information will be propagated throughout
the web of type-constraints, allowing the call-site to extract precisely-typed
results. The binding of such parametric modules will result in a bi-directional
flow of type-information, yielding solutions such as the “most
general intersecting type”, computed using unification algorithms.
Throughout my work in this area, I have been standing on the shoulders
of giants. I owe particular thanks to Willam Cook, Kim Bruce and Luca
Cardelli for formative conversations in the early 1990s and occasional
exchanges since then. If you have been stimulated by this informal
series of articles on the typing and semantics of object-oriented languages,
the next stage might be to get to grips with the details of the type
rules, perhaps in [13, 16]. If you have comments, insights or critiques
to make, please feel free to contact me by email. If you would like
to help bring about the “language with class”, then I have
a PhD project in this area that needs a good student.
Footnotes
1 By this, we mean languages with
second-order type systems; the kind of type aliasing performed in first-order
subtyping is not technically polymorphism, but something much weaker.
2 If you systematically substitute
type X by type Y within some scope, then all Xs must change into Ys.
But with type parameters, you can declare different parameters P <#
X and Q <# X, choosing to substitute {Y/P} and {Z/Q}, so this gives
you slightly finer control over which substitutions happen together.
REFERENCES
[1] A J H Simons, “The theory of classification, part 4: Object
types and subtyping”, Journal of Object Technology, 1(5),
November-December 2002, pp 27-35 http://www.jot.fm/jot/issues/issue_2002_11/column2/index_html
[2] A J H Simons, “The theory of classification, part 7: A class
is a type family”, Journal of Object Technology, 2(3), May-June
2003, pp 13-22, http://www.jot.fm/issues/issue_2003_05/column2
[3] A J H Simons, “The theory of classification, part 19: The
proliferation of parameters”, Journal of Object Technology,
4(5), July-August 2005, pp 37-48, http://www.jot.fm/issues/issue_2005_07/column4
[4] A J H Simons, “The theory of classification, part 8: Classification
and inheritance”, Journal of Object Technology, 2(4), July-August
2003, pp 55-64, http://www.jot.fm/jot/issues/issue_2003_07/column4/index_html.
[5] P Canning, W Cook, W Hill, W Olthoff and J Mitchell, “F-bounded
polymorphism for object-oriented programming”, Proc. 4th
Int. Conf. Func. Prog. Lang. and Arch. (Imperial College, London, 1989),
273-280.
[6] A J H Simons, “The theory of classification, part 18: Polymorphism
through the looking glass”, Journal of Object Technology,
4 (4), May-June 2005, pp 7-18, http://www.jot.fm/issues/issue_2005_05/column1
[7] A J H Simons, Low E-K and Ng Y-M, “An optimising delivery
system for object-oriented software”, Object-Oriented Systems,
1 (1), (1994), 21-44.
[8] C Chambers and D Ungar, “Iterative type analysis and extended
message splitting: optimizing dynamically-typed object-oriented programs”,
Proc. 5th ACM Conf. Prog. Lang. Design and Impl., pub. ACM Sigplan
Notices, 25(6), (1990), 150-164. Reprinted in: Lisp and Symbolic
Computation,
4(3), (1991), 283-310.
[9] A J H Simons, “The theory of classification, part 16: Rules
of extension and the typing of inheritance”, Journal of Object
Technology, 4 (1), January-February 2005, pp 13-25, http://www.jot.fm/issues/issue_2005_01/column2
[10] A J H Simons, “The theory of classification, Part 17: Multiple
inheritance and the resolution of inheritance conflicts”, Journal
of Object Technology, 4 (2), March - April 2005, pp 15-26, http://www.jot.fm/issues/issue_2005_03/column2.
[11] K Bruce, J Crabtree, A Dimock, R Muller, T Murtaugh and R van
Gent, “Safe and decidable type checking in an object-oriented
language”, Proc. 8th ACM Conf. Obj.-Oriented. Prog. Sys., Lang.
and Appl., (1993), 29-46.
[12] K Bruce, A Schuett and R van Gent, “PolyTOIL: A type-safe,
polymorphic object-oriented language,” ACM Trans. Prog. Langs.
and Sys., 25(2), March (2003), 225-290.
[13] K B Bruce, Foundations of Object-Oriented Languages: Types
and Semantics, (Cambridge MA: MIT Press, 2002).
[14] K Bruce, A Fiech and L Petersen, “Subtyping is not a good ‘match’ for
object-oriented languages”, Proc. European Conf. Obj.-Oriented
Prog., pub. LNCS, 1241, (New York: Springer Verlag, 1997), 104-127.
[15] J Palsberg and M I Schwartzbach, Object-Oriented Type Systems (Chichester: John Wiley, 1994).
[16] M Abadi and L Cardelli. A Theory of Objects. Monographs
in Computer Science, Springer-Verlag, 1996.
About the author
|
 |
Anthony Simons is
a Senior Lecturer and Director of Teaching Quality in the Department
of Computer Science, University of Sheffield, where he leads object-oriented
research in verification and testing, type theory and language
design, development methods and precise notations. He can be reached
at a.simons@dcs.shef.ac.uk. |
Cite this column as follows: Anthony J H Simons: “The Theory
of Classification Part 20: Modular Checking of Classtypes”, in
Journal of Object Technology, vol. 4, no. 17, September-October 2005,
pp. 7-18 http://www.jot.fm/issues/issue_2005_09/column1
|
