The Theory of Classification
Part 18: Polymorphism
through the Looking Glass
Anthony J H Simons, Department of Computer Science, University
of Sheffield
|
 |
COLUMN
PDF Version |
1 INTRODUCTION
In this, the eighteenth article in a regular series on object-oriented
type theory, we look at how object-oriented languages might evolve
in the future, given that the formal notion of class is now
better understood than at the outset. Object-oriented languages were
the first
family to suppose that there might be systematic sets of relationships
between all the program data types and use this as the basis for a
kind of type compatibility. However, the early formal models chosen
were based on simple types and subtyping [1] and struggled in practice
to support all the obvious, systematic relationships that programmers
intuitively recognised [2]. For a while, objects were thought to have
class and type independently, where class was
demoted to a mere implementation construct. Later, it was realised
that the notion of class is
also a typeful construct that requires at least a bounded second-order  -calculus
model to explain it [3]. We have developed this model in the Theory
of Classification, showing how it deals properly with typed inheritance
[4, 5] and generic types [6] in a consistent framework.
However, current object-oriented languages fall short of what is
actually possible in a language that really supports the notion of
class. The
majority still treat classes for the most part as if they were the
same thing as simple types, and it only becomes clear that something
more sophisticated is intended when dynamic binding in these languages
is examined, showing dispatching behaviour equivalent to higher-order
functions [7]. The additional template mechanisms of C++ and Java
(from version 1.5) are intended partly to compensate for the lack of
expressiveness
caused by treating classes as simple types. But do we really need
all these separate typing mechanisms? What would a language look like
that
consistently supported the higher-order notion of class throughout?
2 THE HALFWAY HOUSE
In the very first article of this series [8], we described three increasingly
more flexible kinds of plug-in type compatibility, in the context of
supplying a component to match 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.
An example of correspondence is the strong monomorphic typing exhibited
in languages like Pascal or Modula-2, in which every object is of a
single type and may only be passed to variables of exactly the same
type. Pascal’s strong name equivalence rule means that even structurally
equivalent types are considered distinct, if their type names are distinct
(in contrast to C++’s typedefs, which are only aliases for the
base type).
An example of subtyping is where a subrange object is coerced to
a base type variable, so that the base type’s function may be
executed, such as where two SmallInt objects are passed to an Integer
plus function
and the result is returned as an Integer. The function originally expected
Integers, but could handle subtypes of Integer and convert them. Note
that no dynamic binding is implied or required. Also, a simply-typed
first-order calculus (with subtyping) is adequate to explain this behaviour.
An example of subclassing is where the functions of the interface
are systematically replaced by functions appropriate to the new type,
such
as where a Numeric type’s abstract functions plus,
minus, times and divide, are replaced by retyped versions for a Complex type. Rather
than coerce a Complex object to a Numeric, the call to plus through
Numeric executes the replacement Complex plus function. This could
be achieved through dynamic binding; or alternatively through template
instantiation (in which the parameter Numeric is replaced throughout
by an actual Complex type), requiring at least a second-order calculus.
What are the important differences between the simple subtyping and
subclassing approaches? In the subtyping approach, the Integer
plus function treats its SmallInt arguments
exactly as if they were plain
Integers. It returns a result of the general type Integer and
does not know or care whether the result is still in the range of a SmallInt.
On the other hand, in the subclassing approach, there is an obligation
to propagate type information about the actual argument and result
types of Complex's plus back to the call-site. Whereas the
interface expected a Numeric, once this was bound to a Complex number,
the second argument was also forced to be a Complex number.
Furthermore, the result-type, which was formerly Numeric,
is now known also to be of the Complex type. This
means that the caller of plus must
know how to deal with more specific types than originally specified
in the interface. From
our point of view, this is exciting stuff, in the true spirit of classification,
and something worth exploiting in the design of object-oriented languages.
However,
the majority of languages only practise a halfway-house approach, which
is subtyping with dynamic binding. This is similar to subtyping,
except that the subtype may provide a replacement function that is
executed instead. Recalling the earlier example, this is like the SmallInt type providing its own version of the plus function which wraps the
result back into the SmallInt range. Syntactically, the result is acceptable
as an Integer, but semantically it may yield different results from
the original Integer plus function (when wrap-around occurs). From
the type perspective, we still only know that the result is of the
Integer type (rather than SmallInt) because there is no way of propagating
type information about the actual arguments through to the result of
the function. So, we have a situation where more specific functions
are executed, but externally we cannot see that their type has changed.
This gives rise to the phenomenon of “type loss” in C++
and Java, requiring corrective use of type downcasting to recover the
most specific types of returned objects [2].
3 POLYMORPHISM REVISITED
Stopping at the halfway house constitutes a failure of nerve in the design
of object-oriented languages. At the heart of this problem is the inability
to distinguish the notions of class and type in the syntax of programming
languages. If an object-oriented language implemented this distinction
properly, a programmer should never have to perform type downcasting, but
the language could always recover the most specific types of returned objects
for itself. To make this distinction absolutely clear, in the Theory
of Classification:
- a type always refers to a simple monomorphic type, a first-order
construct;
- a class always refers to a polymorphic type, a second-order
(or higher) construct.
As stated previously [8], the term polymorphism has less to do with
the dynamic binding of methods and properly describes the generalised
types of variables that may receive values of more than one type.
In conventional programming languages, we consider that type constructors,
such as
Stack[T] or Map[K,V] are polymorphic, because they contain type variables
standing for possibly many types, and may be adapted to specific
types by parameter
instantiation. In object-oriented languages, we also consider that
a variable of “class-type” is polymorphic and can be made to receive actual
objects of possibly many types, where these are restricted by the class
hierarchy to be of some “subclass-type” of the target variable.
These polymorphic mechanisms seem on the surface to be quite different,
but they are fundamentally the same.
In the -calculus, polymorphism always requires a type parameter,
standing for the generalised type; and when a polymorphic variable
binds to a specific type, this type is propagated into the parameter,
throughout the whole parameterised expression. The formal model
therefore brings
together
the notions of class-based polymorphism and template-based polymorphism.
In earlier articles [2, 3], we deliberately drew out the similarity
between classical Girard-Reynolds [9, 10] univeral polymorphism:
in which you could give functions truly generalised
types (where ? ranges over absolutely any type) and Cook et al.’s
[11, 12] function bounded polymorphism:
in which you could give functions class-types (where  ranges over only those types which have at least the functions specified in the interface
of the bounding generator function). F-bounded polymorphism is more general
than universal polymorphism (since you can type more things using F-bounds,
for example you can type SortedLists of Comparable elements with F-bounds,
whereas you can only type plain Lists of universal elements, without them).
This can be shown formally by recasting Girard-Reynolds polymorphism as
a special case of F-bounded polymorphism:
That is, we constrain to
range over those types which have at least the functions of the universal
interface, but this
interface is trivial (empty), so ranges
again over any type.
There are two practical consequences of this discussion. The first
is that, wherever a polymorphic variable is required in our programming
language, we should always model its type using some kind of type parameter
in the formal calculus. The fact that object-oriented languages don’t
make the type parameters explicit for their classes is one of the reasons
why the notions of class and type get so confused. The second is that
we do not need separate mechanisms to explain template-based and class-based
polymorphism. The class parameters constrained by F-bounds are adequate
for both purposes [6], being more general than classical unconstrained
parameters.
4 DISTINGUISHING CLASS AND TYPE
In current object-oriented languages, objects and variables are “typed” using
the names of the classes like type identifiers. These identifiers
are used ambiguously, to describe either an object or value with an exact
type (a
monomorphic type in the theory), or, alternatively, to describe a
variable with a flexible type (a polymorphic class in the theory). What
we should
like is for object-oriented languages to indicate a class, or a type unambiguously.
Informally, it is possible to infer the intended semantics
of class
identifiers from the program context in which they appear. In a
C++ or Java-like language, when we create an object, we usually intend
to create
something with a fixed implementation and an exact type:
In this context, we do not expect to obtain some instance
of a subclass of Point, but rather an exact instance of the exact type
Point. On the other hand, when we declare a program variable of the Point class, it is clear that we intend this to be flexible, capable of receiving
values that might be more specific than a Point, but which are at least
of this class:
In this context, we do not expect these variables
to be restricted to accepting only objects of the exact Point type,
but rather any type which is at least a subclass of Point.
We can model these differences in the -calculus, to make them explicit.
Recall that a class is defined essentially as a flexible, open-ended
implementation, parameterised by self, with a corresponding polymorphic
type, parameterised by  , the self-type [4]. We give the type-shape
of the class using a type generator, followed by the implementation-shape
using an object generator, which is typed using the type generator
as the F-bound, restricting what types may eventually replace the
self-type:
In our C++ or Java-like programming language,
when we declare a variable of the Point class, what we are
really asserting is the polymorphic typing p0 : ,
where is a type parameter
constrained to range over any type in the Point class:
| Programming Language |
Formal Model |
 |
 |
Table 1: Polymorphic variable declaration
On the other hand, when we create an exact instance of the Point type,
we must fix both the type and the implementation. In the calculus,
this is done by taking the fixpoint of the type generator and of the
object generator [4]:
This creates the exact instance aPoint of the exact Point type. We
can therefore model the meaning of object creation expressions in our
programming language:
| Programming Language |
Formal Model |
 |
 |
Table 2: Exactly-typed object creation Here,
we have taken the liberty of introducing the temporary variable p1 in the formal model, so that we can initialise this variable to the
rather complex object creation expression and then see that it has
an exact type, which is the Point type we expected. The temporary variable
is simply a convenience, to save repeating longer expressions. In section
6 below, we will use a similar approach to analyse program behaviour
in step-by-step detail.
5 TYPE CHECKING WITH FIRST-ORDER TYPES
First, we shall introduce a test-case that exemplifies some of the
difficulties identified with type systems that check types in the first-order
model (with simple types and subtyping). The example code fragment,
expressed in our C++ or Java-like language, is a cut-down version of
the infamous “Eiffel type failure” problem first identified
by Cook [13]:
Programmers expect a Point3D instance to be type-compatible with a
Point variable, but in the first order model, this is not the case.
To explain why the above fragment is problematic, we should define
the Point3D class, which describes a three-dimensional point, whose
interface extends that of a standard two-dimensional Point:
In particular, an instance aPoint3D : Point3D,
created from these generators by taking the fixpoints (see section
4) will have an extra z field; and when aPoint3D tests itself for equality
against another point, it will compare all of its x, y and z fields.
In the original “type failure” scenario, the programming
language expected the subtyping relationship Point3D <: Point to
hold. In fact, we now know that these types are not in a subtyping
relationship, because the retyping of Point3D’s equal method
violates the function subtyping rule [1]. However, Eiffel allowed subclasses
to retype their methods with more specific argument types, since it
is unlikely in practice that we should want a Point3D to compare itself
with more general kinds of point.
An undetected type failure arises as follows. First, we create a
specific Point3D instance and assign it (by polymorphic aliasing)
to the more
general variable p : Point. This is permitted by the (faulty)
assumption that Point3D <: Point. Then, we create another
instance q
: Point.
Finally, we invoke p.equal(q), at which moment the undetected
type failure occurs. Statically, the type of equal is Point.equal
: Point  Boolean,
so it appears to be legal to pass in the given argument q : Point.
However, p currently contains a dynamic instance of Point3D and
the version of the equal method which is actually invoked is Point3D.equal
: Point3D Boolean.
This receives the too-general argument q : Point, and during the execution
of the method body, an attempt
is made to
access the z field of a plain Point, which will cause the program to
crash, generating a memory segmentation fault.
Cook originally proposed to fix this problem by forcing Eiffel to
conform to strict subtyping rules [13]. Redefined argument types for
equal would therefore not be allowed. Although this technically satisfies
subtyping, we have seen how this results in a strictly less expressive
language [2]. In particular, the equal method, which is required
by every class, may only be typed with the most general kind of argument
(usually, the root class Object), and it may never be retyped with
more restricted types of argument. Instead, redefined versions of
equal have to accept Object arguments and use runtime-checked type downcasting
internally, to recover the more specific dynamic type of the argument,
before comparison can be made. This merely pushes the type failure
problem back into the run-time.
6 TYPE CHECKING WITH SECOND-ORDER CLASSES
Classes are type-recursive, meaning that their methods often accept
or return arguments of the self-type. So it is natural to want these
arguments and results to become uniformly specialised along with the
class itself. We want to allow a Point3D to specialise the argument
type of its equal method. However, we still want to avoid unchecked
type failures.
In the Theory of Classification, we take the
view that a class is not a first-order concept, but a second-order,
polymorphic concept. One of the advantages this brings is the ability
to relate closed recursive types to each other, by relating their generators
in a (second-order) pointwise subtyping relationship [3]. This allows
us to specialise argument and result types uniformly, in line with
programmers’ intuitions about classes. However, the recursive
types themselves do not enter into simple subtyping relationships,
so we cannot type-check them in the usual first-order system. By properly
distinguishing the polymorphic notion of class from the monomorphic
notion of type, we may type-check the same fragment of object-oriented
code in a second-order model, showing that polymorphic assignment really
involves the propagation of types into polymorphic type parameters.
This is a very powerful checking mechanism, capable of resolving many
of the difficulties formerly identified with object-oriented type systems.
On the left-hand side of table 3, the expressions in the programming
language are broken down into small steps, in order to examine the
types of these expressions in the formal model on the right-hand side.
On the first row, we declare a polymorphic Point variable and show
this to have a F-bounded parametric type. On the second row, we create
an exact Point3D object and show this to have the exact Point3D type.
On the third row, we assign the specific instance to the general variable.
This is where the new type-checking principle first comes into play.
At the moment of polymorphic aliasing, the exact type of the object
is propagated into the type parameter of the variable, shown by the
substitution: {Point3D / }. As a consequence, we obtain a new context
p2 after the assignment (p0 := p1), in which the type of the bound
variable expression has been updated.
This is how the type mismatch is eventually detected. When checking
the program expression: p.equal(q), the model can predict
the type of the equal method, and its expected argument type,
since statically it knows that this is selected from p2. At
the same time, the model knows the type of the actual argument, from
the context q2. The formal
and actual argument types are shown to conflict (Point  Point3D),
so the checker can raise a type mismatch at compile time. Not only
do we spot the type error at compile time, but we do this without having
to restrict the expressiveness of the language. We still allow Point3D objects
to be passed into polymorphic variables p : <:
GenPoint[, so long
as this does not conflict with other typing requirements further
down the line. For example, the following code fragment is readily
accepted by this checking algorithm:
since, at the moment of selection, the equal
method has the type Point3D.equal : Point3D Boolean.
As a consequence, it can happily accept the actual argument q :
Point3D.
The following
code fragment is also acceptable:
because the type substitution {Point3D / <:
GenPoint[]} is made consistently when both p and q alias values of
exact types, before the typing of the equal method invocation is considered.
Though the variables p, q were originally declared with general polymorphic
types, new type contexts are established by the polymorphic aliasing.
7 CONCLUSION
Any object-oriented language that truly supports the notion of class should
be able to distinguish contexts where simple types, or polymorphic classes
are intended. The secret to success is to preserve the underlying type parameter
in expressions where polymorphism is intended. When polymorphic variables
alias each other, this has the effect of substituting one type parameter
for another, possibly strengthening the F-bound constraint (this is because
unifying two type variables requires that you accept the more restricting
of the two type constraints – see the previous discussion on intersection
types in [5]). When polymorphic variables alias objects with exact
types, these types are substituted into the type parameters. As a consequence,
it
is always clear whether an expression has a polymorphic, or fixed type,
in a given context.
Object-oriented lanaguages that adopted this simple rule could remove
a lot of clutter from their syntax. To start with, there would be no
need to have both this kind of (genuine) polymorphic typing and subtyping.
So,
type checkers that performed parametric substitutions would not also
have to perform subtyping coercions. If two simple types turned out
not to be
the same, the checker could immediately rule them as mutually incompatible!
Secondly, there would be no need for separate syntactic treatments
of template-based and class-based polymorphism, since both would be
handled using the same
underlying F-bounded parametric mechanism. However, the type instantiation
process might happen at run-time as well as at compile-time (this unifies
the notions of dynamic binding and template instantiation). Thirdly,
we would have to consider more carefully the scope of type substitutions
made when
polymorphic aliasing occurs. We would expect, for example, that a polymorphic
method would bind type parameters on entry, but release these bindings
on exit, so that the method could be applied to an object of some different
type on another occasion. What then is the scope of a polymorphic assignment?
We saw above that binding one type rules out subsequent assignments
to different
types. The scope of an assignment would have to be defined carefully,
with rules for “undoing” an assignment and recovering the old
polymorphic type of the variable.
The advantages of (genuine) polymorphic typing do not stop there. For
example, type propagation may have considerably stronger and pervasive
effects on the behaviour of a piece of software. The C++ Standard
Template Library
makes use of this when it defines template allocators for handling
the memory management aspects of regular data types. Substituting
different actual allocators
can alter the efficiency of the whole program. In fact, parametric
substitution is related to reflective meta-programming and, when
properly exploited, can
produce most of the pervasive benefits claimed by aspect-oriented
programming. By understanding the true polymorphic nature of the class, we may yet
obtain much simpler, yet more powerful programming languages.
REFERENCES
[1] A J H Simons, “The theory of classification, part 4: Object types
and sub-typing”, Journal of Object Technology, vol.1 no.5, November-December
2002, pp 27-35. http://www.jot.fm/issues/issue_2002_11/column2
[2] A J H Simons, “The theory of classification, part 7: A class is
a type family”, Journal of Object Technology, vol.2 no. 3, May-June
2003, pp 13-22. http://www.jot.fm/issues/issue_2004_05/column2
[3] A J H Simons, “The theory of classification, part 8: Classification
and in-heritance”, in Journal of Object Technology, vol. 2, no. 4,
July-August 2003, pp. 55-64. http://www.jot.fm/issues/issue_2003_07/column4
[4] A J H Simons, “The theory of classification, part 11: Adding class
types to object implementations”, in Journal of Object Technology, vol.
3, no. 3, March-April 2004, pp. 7-19. http://www.jot.fm/issues/issue_2004_03/column1
[5] A J H Simons, “The theory of classification, part 16: Rules of extension
and the typing of inheritance”, in Journal of Object Technology, vol.
4, no. 1, January-February 2005, pp. 13-25. http://www.jot.fm/issues/issue_2005_01/column2
[6] A J H Simons, “The theory of classification, part 13: Template classes
and genericity”, in Journal of Object Technology, vol. 3, no. 7,
July-August 2004, pp. 15-25. http://www.jot.fm/issues/issue_2004_07/column2
[7] W Harris, “Contravariance for the rest of us”, Journal
of Object-Oriented Programming, Nov-Dec 1991, 10-18.
[8] A J H Simons, “The theory of classification, part 1: Perspectives on
type compatibility”, Journal of Object Technology, vol. 1 no.
1, May-June 2002, pp 55-61. http://www.jot.fm/issues/issue_2002_05/column5
[9] J-Y Girard, Interpretation fonctionelle et elimination des coupures
de l'arithmetique d'ordre superieur, PhD Thesis, Universite Paris VII,
1972.
[10] J Reynolds, Towards a theory of type structure, Proc. Coll. Prog.,
New York, LNCS 19 (Springer Verlag, 1974), 408-425.
[11] 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.
[12] W Cook, W Hill and P Canning, “Inheritance is not subtyping”,
Proc. 17th ACM Symp. Principles of Prog. Lang., (ACM Sigplan, 1990),
125-135.
[13] W Cook, “A proposal for making Eiffel type safe”, Proc.
3rd European Conf. Object-Oriented Prog., 1989, 57-70; reprinted in Computer
Journal 32(4), 1989, 305-311
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 Simons: “The Theory
of Classification Part 18: Polymorphism through the Looking Glass",
in Journal of Object Technology,
vol. 4, no. 4, May-June 2005, pp. 7-18 http://www.jot.fm/issues/issue_2005_03/column1
|
