\documentstyle[a4wide,11pt,snamed,tapos]{article}

\author{Andreas Gawecki \and Florian Matthes}

\title{TooL: A Persistent Language Integrating \\
Subtyping, Matching 
and Type Quantification\thanks{
This research is supported by ESPRIT Basic Research, Project FIDE,
\#6309 and by a grant from the German Israeli Foundation for Research
and Development (\e{bulk data classification}, I-183 060).
}}

\date{{\small Universit\"at Hamburg\\Vogt-K\"olln Stra{\ss}e 30\\D-22527 Hamburg, Germany\\
      {\{gawecki,matthes\}@informatik.uni-hamburg.de}}}
 
\sloppy
\frenchspacing

\begin{document}

\parskip 1.5ex
\parindent 0ex

\maketitle

\begin{abstract}
\noindent This paper presents the type system of the TooL 
persistent programming language that captures much of the flavor of
Smalltalk within a safe static typing discipline.  Following the spirit
of Smalltalk providing a highly flexible and extensible programming
environment based on a small set of expressive language primitives,
TooL provides only few built-in type concepts with rich semantics that
achieve power through systematic use and orthogonality.  The paper
focuses on the language design issues that arise in the course of
integrating type concepts that are well-understood in isolation like
object types, subtyping, type matching, and type quantification into a
practical database programming language.  We illustrate these issues by
code samples taken from the TooL generic bulk data library.
\end{abstract}

\vspace*{5cm}

\ \\

\pagebreak
\tableofcontents
\pagebreak


\section{Introduction}

The design and implementation of the persistent Tycoon object-oriented
language TooL is heavily influenced by language design experience gained
in the Tycoon project carried out at Hamburg University. The
Tycoon\footnote{TYped Communicating Objects in Open eNvironments}
project follows an \e{add-on} approach to generic database programming
that emphasizes type-safe scalability and extensibility
\cite{MaSc93b,Matt93}.

At the system level, Tycoon offers orthogonal persistence and support
for distribution and migration of data, code and threads between
persistent address spaces in local and wide area networks \cite{MaSc94,MMS95}.
Moreover, bidirectional gateways to external languages can be realized
systematically.  These gateways are captured at the language level as
polymorphically typed generic libraries \cite{MMS94}.

The rationale behind the original Tycoon type system is to provide a set of 
unbiased, orthogonal primitives to support multiple database programming 
methodologies like functional, imperative and different flavors of 
object-oriented modeling.  Tycoon is based on function types, record types, 
and recursive types in a full higher-order type system where subtyping and 
unrestricted existential and universal quantification is provided over 
types, type operators and higher-order type operators, including a limited 
form of dependent types.  Tycoon is therefore similar to Quest
\cite{Card90,CaLo91} and  the type theoretic model of
$F_{<:}^{\omega}$ \cite{PiTu93b} but it avoids the notion of kinds
(types of types) by generalizing subtyping to higher-order types.

Unfortunately, the expressiveness of Tycoon's type system does not
suffice to adequately capture the notion of type \e{matching}
\cite{BlHu90,Bruc93,Bruc95,AbCa95}, even by complex higher-order
encodings.  Matching supports type-safe inheritance of binary methods as
it is required for pure object-oriented modeling and for the
construction of reusable bulk data libraries \cite{MaSc91b}.

In this paper, we describe the design rationale and type system of TooL
that has a strong bias towards a pure object-oriented programming
methodology in the spirit of Smalltalk but otherwise adopts most of the
Tycoon principles outlined above.  TooL aims for expressive power by the
systematic use and orthogonal combination of few semantically rich
primitives: Object types combine aggregation, encapsulation, recursion,
parameterization and inheritance.  At the type level there are two
inductively defined, structural orderings on types (subtyping and
matching) and universal type quantification (parametric polymorphism)
that can be combined in interesting ways that we discuss by examples
from the TooL bulk type library in this paper.

This paper is structured as follows. After an overview of the language
and a description of its underlying design principles in section 2, we
present TooL's fundamental typing concepts in section 3.  The following
section illustrates how to exploit these polymorphic typing concepts for
the construction of pure object-oriented class libraries using
inheritance. Again, the interaction between subtyping and matching is of
particular interest. The remaining sections report on the TooL system
implementation, provide a comparison with related research, and point out
future work.

\section{TooL Design Rationale and Language Overview}

Since the focus of the Tycoon project is not to verify type-theoretic
concepts but to develop a fully-fledged persistent programming
environment, we highlight in this section the design principles behind
the TooL language.

TooL minimizes built-in language functionality in favor of flexible
system add-ons, both at the level of values and at the level of types.

\TooL\ supports the classical object model where objects are viewed as
abstract data types encapsulating both state and behavior.  Similar to
Smalltalk \cite{GoRo83} and Self \cite{UnSm87}, TooL is a \e{pure}
object-oriented language in the sense that \e{every} language entity is
viewed as an object and \e{all} kinds of computations are expressed
uniformly as (typed) patterns of passing messages \cite{Hewi77}.  Even
low-level operations like integer arithmetic, variable access, and array
indexing are uniformly expressed by sending messages to objects.

Contrary to other statically-typed object-oriented languages and
specification languages \cite{Gogu90}, TooL provides statically-scoped
higher-order functions that are also viewed as first-class objects that
understand messages. Thereby control structures like loops,
conditionals, function calls and exception handling also do not have to
be built into the language, but can be defined as add-ons using objects
and dynamic binding.

To improve code reusability, even the access to instance and pool
variables (that unify the concept of global and class variables in
Smalltalk) is done by sending messages \cite{John88}. This obviates the
need for special scoping and typing rules concerning instance and pool
variables.

TooL's simplicity at the value level leads to a significant complexity
reduction at the type level where it is only necessary to define type
and scoping rules for class signatures, message sends and inheritance
clauses which we explore in the rest of the paper.

Despite the semantic simplicity of TooL, there is a rich set of
syntactic variants to write down message sends. This syntactic sugar
helps to define compact yet easy to read message patterns, for example
to capture control structures or arithmetic computations. For
``power-users'' developing domain-specific abstractions (like query
language notations or concurrency control schemes), the TooL language is
based on extensible grammars \cite{CMA94} to enable dynamic syntax
extensions.

Finally, it should be noted that modern compiler technology eliminates
most of the run-time performance overhead traditionally associated with
the pure object-oriented approach \cite{ChUn91,Hoel94,Gawe91a}. For
example, TooL uses dynamic optimizations across abstraction barriers
based on persistent CPS representations to ``compile away'' many message
sends \cite{GaMa95}.

%advantages of Int, Char etc. as Objects: \cite{GoRo83}


\section{TooL's Basic Typing Concepts}

The \TooL\ language is strongly and statically typed in the sense that
no operation will ever be invoked on an object that does not support it,
i.e. errors like ``message not understood'' cannot occur at run time. In
this section we motivate and describe TooL's basic typing concepts,
namely modular and structural type-checking, as well as subtyping and
matching. To formalize these concepts, we have defined a full set of
natural deduction-style type rules on the abstract TooL syntax
\cite{GMS95} in the spirit of \cite{MTH90} and \cite{MaSc92a}. In the
remainder of the paper we restrict ourselves to an informal discussion
of the finer points of these type rules.

\subsection{Type-Checking in Persistent and Distributed Environments}

TooL programs are executed in a persistent and distributed enviroment
where it is necessary that software components can be developed and
maintained independently (over time and across space) which leads to the
following requirements.

\begin{description}

\item[Structural Subtyping:] Several conventional object models couple
the implementation of an object with its type by identifying types with
class names (e.g. C++, ObjectPascal, Eiffel). In these models, an object
of a class named $A$ can only be used in a context where an object of
class $A$ or one of its statically declared superclasses is
expected. This implies that type compatibility is based on a single
inheritance lattice which is difficult to be maintained in a persistent
and distributed scenario.

Therefore, \TooL\ has adopted a more expressive notion of type
compatibility based on \e{structural subtyping} (called \e{conformance}
in \cite{Hutc87}). Intuitively, an object type $A$ is a subtype of
another object type $B$ when it supports at least the operations
supported by $B$. That is, \TooL\ views types as (unordered) sets of
method signatures, abstracting from class or type names during the
structural subtype test.  The additional flexibility of structural
subtyping is especially useful if $A$ and $B$ have been defined
independently, without reference to each other. Such situations occur in
the integration of pre-existing external services, in the communication
between sites in distributed systems \cite{BNOW93}, and on access to
persistent data \cite{ACPP90}.

%ACPP90 xx bessere Referenz in ACM TOPLAS oder so

\item[Modular Type-Checking] of a class only requires access to the
interfaces of imported classes and of superclasses. In particular, it
should be possible to type-check new subclasses without having to
re-check method implementation code in superclasses again. Modular type
checking speeds up the type-checking process significantly, thus
supporting rapid prototyping within an incremental programming
environment. It also has the advantage that class libraries -- developed
independently by different vendors -- can be delivered in binary form
without (a representation of) their source code with the option of
type-safe subclassing at the customer side.

Modular type-checking requires the {\em contravariant} method
specialization rule for soundness, which means that the types of method
arguments are only permitted to be generalized when object types are
specialized.  The contravariant rule has been criticized of being
counter-intuitive \cite{Mey89}. Accordingly, Eiffel has adopted a {\em
covariant} method specialization rule which requires some form of global
data flow analysis at link-time to ensure type correctness. Such an
analysis (besides being time-consuming) generally requires the source
code (or a close representation of it) of all classes and methods that
constitute the whole program to be available to the type-checker at
link-time which is not acceptable in our setting. TooL provides a
partial solution to the covariance/contravariance problem without giving
up modular type-checking by adopting the notion of \e{type matching}
which allows the covariant specialization of method arguments in the
important special case where the argument type is equal to the receiver
type.

\end{description}

\subsection{Structural Subtyping}

The most important application of subtyping is {\em subsumption} or {\em
substitutability}: we may use an object of a subtype in situations where
an object of some of its supertypes is expected. Another application of
subtyping in TooL is bounded type quantification as discussed in section
\ref{Sec:PolyMethods} and \ref{Sec:ClassParameters}.

As an example for substitutability, consider the \p{printOn} method
defined in class \p{Object} to print any TooL object onto a stream of
characters:
\begin{xple}
class Object
  printOn(aStream :WriteStream(Char))
\end{xple}
For example, we may send a string literal object the message \p{printOn}
to print itself onto the object \p{stdout} (standard output) which is an
instance of the class \k{File}.
\begin{xple}  
"a string".printOn(stdout)
\end{xple}
In order to substitute a file in a context where a write stream of
characters is expected, we have to show the subtype relationship
\hbox{\p{File \subtype\ WriteStream(Char)}}.

In TooL, it is not required that an explicit inheritance relationship
between these two classes exists.  The subtype relationship holds
implicitly and can be deduced from the structure of the following class
interfaces:
\begin{xple}
class WriteStream(E \subtype Object)
  put(e :E) :Void 

class File
  get :Char
  put(ch :Char) :Void
  close :Void 
\end{xple}
The generic class \p{WriteStream} is parameterized with an element type
\p{E} that is bounded by the type \p{Object} (cf. section
\ref{Sec:ClassParameters}) and exports a single 
method \p{put} to append an object \p{e} of type \p{E} to the stream.
The independently defined, unparameterized class \p{File} also exports a
\p{put} method that takes only characters in addition to a \p{put} and
\p{close} method.

Subtyping is transitive and reflexive and the TooL subtype lattice
contains all closed object types which correspond to non-parameterized
class interfaces.  For convenience, TooL class definitions implicitly
define a corresponding object type and there is no extra syntax in TooL
to define object types (e.g. as in PolyTOIL \cite{Bruc95}).

The top element of the subtype lattice is called
\p{Void}, which is an object type with an empty method
suite. Currently, all TooL classes are descendants of a more specialized
class \p{Object} that already provides some core methods (e.g. testing
for object identity and printing).

The bottom element of our type lattice is the type constant \p{Nil}.
The only subtype of \p{Nil} is \p{Nil} itself (due to reflexivity). The
special object \p{nil} (the {\em undefined object}) is the single
instance of this type. Conceptually, the type \p{Nil} consists of an
infinite method suite, supporting any operation with any
signature. However, sending any message to \p{nil} (other than identity
testing and printing) triggers a runtime exception. The value
\p{nil} is used to initialize instance variables and to mark {\em not yet
filled} slots in hash tables. The type \p{Nil} is also used to type
expressions that raise an exception.

% xx Nil important for bound specifications in higher-order subtyping
% involving contravariant type operators.

%cite emerald: much ado about NIL?
% xx There is a separate lattice of parameterized higher-order types xx


\subsection{Type Parameterization}
\label{Sec:PolyMethods}

Classes (as discussed up to now) introduce type constants. Classes can
be turned into {\em generic classes} by type parameterization.
Parameterization is particularly useful when defining generic container
classes.  As a database group, our current research focuses on the
design of a highly reusable container class library with sophisticated
iteration and query facilities, utilizing the advanced typing
capabilities of TooL.

In TooL, parameterized classes are not simple templates that can only be
type-checked after instantiation like in C++ or in Trellis. Type
parameters are {\em bounded} by a type that permits local, modular type
checking within the scope of the quantifier.

In the following example, the element type of sets is parameterized, but
constrained to be a subtype of \p{Object} in order to allow some basic
messages to elements (e.g.  comparisons for object identity and
printing):
\begin{xple}\label{xple:set}
class Set(E \subtype Object)
  add(e :E) :Void
  includes(e :E) :Bool
  inject(F \subtype Object, unit :F, f :Fun(:F, :E):F) :F
  printOn(aStream :WriteStream(Char))
\end{xple}
This class interface shows that type parameterization is also available
in individual method and function signatures, like in the higher-order \p{inject}
method that iterates over all elements of type \p{E} within the set,
accumulating the values computed by a binary user-specified function
\p{f} on arguments of type \p{F} and \p{E}, given an initial value
\p{unit} of type \p{F}. 

As can be seen from the example above, TooL incorporates the full power
of bounded parametric polymorphism as found in F$_{<:}$
\cite{CMMS91}. 

TooL provides type argument synthesis in message sends and function
applications which makes it possible to write, for example,
\p{intSet.inject(0, plus)} instead of \p{intSet.inject(:Int, 0, plus)}. 
This is particularly useful in the typing of control structures
modeled with message passing.

Functions do not introduce additional complexity at the type level since
they are treated as objects supporting an apply method. This also scales
to polymorphic and higher-order functions.


\subsection{Type Matching}
\label{Sec:Matching}

In addition to subtyping, TooL provides a second relation between
(usually recursive) object types, called {\it matching} (denoted by \p{A
\matchtype\ B}) which has been proposed
\cite{BlHu90,Bruc93} to overcome some well-known problems with subtyping
\cite{CCHO89}.  In general, matching does not support subsumption (see
section \ref{Sec:SubtypingAndMatching} for a relaxation of this
statement), but it supports the inheritance and specialization of
methods with negative (contravariant) occurrences of the recursion
variable (with {\em binary methods} as a special case).

Intuitively, the matching relation captures certain forms of
self-referential similarity of object types. In the following example, we
define a class \p{Equality} supporting a single infix equality predicate
(\p{"="}):
\begin{xple}
class Equality
  "="(x :Self) :Bool
\end{xple}
The keyword \p{Self} (similar to \p{MyType} in PolyTOIL \cite{Bruc93})
is used in TooL to indicate the self reference of object types
explicitly.

Exploiting the notion of matching in TooL we can write a
generic method \p{"!="} that compares two objects for equality and
returns the negated result. All that is required to know is that both
objects are of some type \p{T} that matches \p{Equality}:
\begin{xple}
"!="(T \matchtype Equality, x :T, y :T)
  \{ !(x = y) \}
\end{xple}
In this example, the method type parameter \p{T} can be instantiated by
arbitrary types that \e{match} the type \p{Equality}, like the
following class \p{Int}, that exports two additional binary infix
operators:
\begin{xple}
class Int
  "="(x :Self) :Bool
  "+"(x :Self) :Self
  "-"(x :Self) :Self
\end{xple}
Note that the \e{contravariant} occurrence of the \p{Self} type in the method
signature of \p{"="} prevents a subtype relationship between \p{Int}
and \p{Equality}.  Therefore, we cannot use subtyping instead of matching
in the signature of \p{"!="} (e.g. \hbox{\p{T
\subtype\ Equality}}) if we want to apply this polymorphic
method to objects of type \p{Int}, instantiating \p{T} with \p{Int}.

Similar to the subtype relation, the TooL matching relation is defined
by structural induction on object types; it is reflexive and transitive
and has \p{Void} and \p{Nil} at its top and bottom element,
respectively. An object type \p{A} matches another object type \p{B}
(denoted by \hbox{\p{A \matchtype\ B})} iff they are subtypes
\hbox{(\p{A \subtype\ B})} under the assumption that the corresponding
\p{Self} types are equal. In the example above, the relationship \p{Int
\matchtype\ \p{Equality}} holds implicitly, again without any explicit declarations
of relationships between these two classes.

As explained in section~\ref{Sec:Inheritance}, the explicit type
quantification in the definition of the method \p{"!="} is usually
avoided by defining \p{"!="} in class \p{Equality} utilizing the
quantification of the \p{Self} type within classes during inheritance.

In class definitions, the TooL programmer has the choice between
implicit recursion by class name (to promote subtyping) and explicit recursion with
the keyword \p{Self} (to enable matching).  For example, one could write
\begin{xple}
class Equality
  "="(x :Equality) :Bool
\end{xple}
to decouple the receiver type of the infix message from its argument
type in future subclasses. Similar design issues are discussed in
section~\ref{Sec:Self}. 


\subsection{Interaction between Subtyping, Matching and Parameterization}
\label{Sec:SubtypingAndMatching}

Up to now, we have only discussed the subtyping and matching relation in
isolation. Since TooL makes heavy use of parameterized types, a given
piece of TooL code typically refers to multiple types and type
\e{variables}, some of which are bounded by matching, others by
subtyping. It is therefore crucial to have expressive type rules that
refer elements in the subtyping and matching lattice.

The following type rule states that we can assume that, within a static
context \p{S}, a type variable \p{X} is a subtype of a given type
\p{T}, if we know that, within the same static context, \p{X} matches an
object type with method suite \p{M}, {\em and} we are able to prove that
this object type is a subtype of \p{T}, whereby all occurrences of
\p{Self} within the method suite have been replaced by \p{X}:

{
\typerule{Match vs. Subtype}
  {\judge{S}{X \matchtype ObjectType(Self)M} \quad
   \judge{S,X \subtype T} ObjectType(Self){\subst{M}{X}{\Self} \subtype T}}
  {\judge{S}{X \subtype T}}
}

From the languages incorporating matching, only TooL and Emerald
\cite{BlHu90} provide such a rule which is generalized to parameterized
types in TooL.  The rule can be viewed as a safe, conservative
approximation of the proof steps taken by the type-checker if the exact
type structure of \p{X} was known.


\leaveout{
Intuitively, this
rule is sound because matching requires that X must
contain at least the methods present in M, and if
ObjectType(Self)A[X/Self] is a subtype of B, X must also contain at
least the methods present in B. This means that X can only be no subtype
of B iff A contains methods with negative (contravariant) occurrences of
\p{Self}. But his case is captured since these have been replaced by X.
}

The above rule can be utilized, for example, to prove the trivial
relationship \p{X \subtype Void} for any type variable \p{X} that is
known to match some object type.  Otherwise, special inference rules
involving the top type \p{Void} would be necessary (as, for example, in
PolyTOIL \cite{Bruc95}).

Unfortunately, the inference rule above is one-way only and there is no
symmetric rule to prove matching of type variables from known subtype
relationships. In particular, we cannot know whether two types match
(say, \p{A \matchtype C}) if the only thing we know about them is that
the smaller one (\p{A}) is a subtype of some other type (say, \p{A
\subtype B}). Even if this other type (\p{B}) is itself a subtype of the
bigger type (i.e. \p{B \subtype C}), the matching relation between these
two types is unknown since the type \p{Self} might have been replaced
with the name of the class without affecting subtyping. In our design
work towards TooL, this deficiency turned out to be the main cause of
problems when integrating subtyping and matching into a single
language. As we will see in the next section, these problems can be
solved by adequate type parameterization.



\section{Reconciling Inheritance and Polymorphism}
\label{Sec:Inheritance}

In this section, we describe how to exploit the basic polymorphic typing
concepts introduced in the previous section for the construction of
object-oriented class libraries using inheritance. Again, the
interaction between subtyping and matching is of particular interest.

In the preceding discussion, classes were introduced mainly as a
mechanism to describe object types. In TooL, classes also serve as
repositories of type and behavior specifications that can be reused and
modified by multiple inheritance.
  
Similar to CLOS \cite{BDG*88}, a TooL class definition may give an
ordered specification of its direct superclasses. Possible inheritance
conflicts (name clashes) are resolved by a linearization of the
inheritance tree (i.e. a class precedence list) performed by a
topological sort on the superclass lattice.  Inheriting from the same
class more than once has no effect: \TooL\ has no repeated inheritance
as in Eiffel \cite{Meye88} or C++ \cite{ElSt90}. Even more elaborated
schemes of conflict resolution are possible, for example allocating
different roles for objects as in Fibonacci \cite{ABGO93}. We chose to
omit such sophisticated features to keep our language simple and to
focus on the typing issues discussed in the subsequent sections.

% xx
%Within a class precedence list, each class that precedes another class
%(i.e. it takes precedence during method lookup) must either {\em match}
%it (if matching is ui. This condition, which is a straightforward generalization of the
%inheritance rules given for TOOPLE \cite{Bruc93} and PolyTOIL
%\cite{Bruc95}, is sufficient to ensure type safety of method updates.


\subsection{Typing Self}
\label{Sec:Self}

During the type-checking of a given TooL class $C$, the method bodies
have to be checked with a certain assumption about the type \p{Self} of
the receiver object denoted by \p{self}. This assumption must take into
account {\em all} possible extensions of $C$ due to subclassing since we
want to perform modular type-checking.

% xx Equality example vorziehen

In most commonly used object-oriented languages (e.g. C++, ObjectPascal,
Modula-3, Eiffel), subclassing means subtyping. In these languages,
\p{Self} is known to be a subtype of the current class\footnote{If the
notion of a type \p{Self} is part of the language at all, which is not
the case in C++, for example.}. We say that \p{Self} is {\em
subtype-bounded} by the type of the current class.

In some newer languages (e.g. TOOPLE \cite{Bruc93}, PolyTOIL
\cite{Bruc95}), the subtype hierarchy (implicitly
defined by the subtype relation '$\subtype$') does not have to be equal
to the class hierarchy (explicitly defined by inheritance declarations):
class {\it specialization} (by inheritance) can lead to {\it
incompatible} types that are not related by subtyping any more. This was
motivated by research results on subtyping and inheritance \cite{CHC90}.

But the inheritance rules do ensure {\em matching} of subclasses in
these languages. This means that the only assumption that can be made
during (modular) type-checking a certain class is that any subclass,
and, therefore, the type \p{Self}, will always match the current class.
From this point of view, the matching relation reflects the restrictions
on constructing subclasses by extension or modification of methods of
the superclass.

This {\em match-bounded}\footnote{We avoid the term {\em F-bounded} here
to prevent confusion about our understanding of matching as higher-order
subtyping (cf. section \ref{Sec:Matching})} \p{Self} typing provides
more flexibility because we are not constrained to produce subtypes
during subclassing. There are, however, situations in which it would be
better to know for sure that subclasses will indeed be subtypes.

Fortunately, it is possible to integrate both kinds of
\p{Self} typing (subtype-bounded and match-bounded) into a single
language, leaving the choice to the programmer. In general, it is useful
to use match-bounded \p{Self} typing in higher classes (supporting
inheritance of methods with contravariant occurrences of
\p{Self}, e.g. binary methods), and switching to subtype-bounded self
typing when going down the inheritance lattice (supporting
subsumption). To provide this flexibility in TooL, the constraint on the
\p{Self} type that is assumed by the type-checker can be specified
explicitly using the following notation:
\begin{xple}
class Equality \ldots
Self \matchtype\ class Equality \ldots
Self \subtype\ class Equality \ldots
Self = class Equality \ldots
\end{xple}
where \p{class Equality \ldots} is equivalent to \p{Self \matchtype\
class Equality \ldots}. We now discuss the advantages and disadvantages
of theses alternatives in turn.

Suppose we have modeled points in the usual way, with coordinates as
slots and an equality operation. We would like to inherit the default
implementation of inequality from our class \p{Equality}, but we
override the default implementation there (that uses simple object
identity):
\begin{xple}
Self \matchtype\ class Equality
  super Object
  "="(x :Self) :Bool \{ self == x \}
  "!="(x :Self) :Bool \{ !(self = x) \}
  
Self \subtype\ class Point
  super Equality
  x :Int
  y :Int
  "="(aPoint :Self) :Bool
    \{ x = aPoint.x \& y = aPoint.y \}
  paint(aPen :Pen) :Void
    \{ aPen.dot(self) \}
    
Self \subtype\ class ColoredPoint
  super Point
  color :Color
  $\ldots$
\end{xple}

In the class \p{Point} (and also in \p{ColoredPoint}), we have
explicitly specified which assumption on \p{Self} the type-checker
should make, i.e. that subclasses will always be subtypes of
\p{Point}. This specification allows us to exploit subsumption with the
receiver object (denoted with the pseudo-variable \p{self}) by passing
it as a parameter to an operation that expects a \p{Point} as an
argument, e.g. the \p{dot} method of \p{Pen}.

The specification that subclasses will be subtypes is, of course,
verified when actual subclassing takes place: no further specializations
of methods with contravariant occurrences of \p{Self} are allowed.  For
example, we may not overwrite the equality method in the subclass
\p{ColoredPoint}, even though we might be tempted to take the color
attribute into account during the comparison:

\begin{xple}
Self \subtype\ BadColoredPoint
  super Point
  color :Color
  "="(aColoredPoint :Self) :Bool
    \{ super."="(aColoredPoint) \& color = aColoredPoint.color \}
\end{xple}

This code fails to type-check in TooL. If the \p{paint} method would be
invoked on such a (incorrectly defined) colored point, the code in class
\p{Point} may break since we pass to the pen an object (i.e. \p{self})
with an interface that does not conform to \p{Point}. The \p{dot} method
of \p{pen} might compare the (incorrectly defined) colored point with
some other (ordinary) point, forcing a runtime error since the other
point does not support colors.

The effect of the above \p{Self} constraint specification is that,
during type-checking subclasses  (e.g
\p{ColoredPoint}) of the given class, all occurrences of \p{Self} in
superclasses are replaced by the corresponding superclass name, turning
explicit self references into implicit ones\footnote{At a first glance,
it seems to suffice to replace the negative (contravariant) occurrences
of \p{Self} only, as proposed in
\cite{ESTZ94}. This would provide more accurate type information in
subclasses for the positive occurrences of
\p{Self} since these would be automatically specialized in subclasses.
However, this approach is unsound if we do not tread positive
(covariant) and negative occurrences of \p{Self} as different types.  We
are currently investigating whether the benefits of such an approach
will outweight the additional complexity of the type system.}.  This
means in particular that a subclass need not match a superclass any more in
TooL. In the above example, \p{ColoredPoint} does not match
\p{Equality} since the \p{Self} argument type of the equality method
(defined in the superclass) has been replaced by \p{Point} (the name of
the superclass) during subclassing. 

Another constraint on the type \p{Self} that can be specified in TooL is
that it will always match the current class. This constraint is the
default in TooL since it is the most flexible one with respect to
subtyping. We specified this constraint on \p{Self} in the class
\p{Equality} above, which permitted us to overwrite the equality method
with contravariant occurrences of \p{Self} in the subclass \p{Point},
producing a subclasses that is not a subtype of \p{Equality}. Note that
we could make the same design decision with class \p{Point}, allowing
further refinement of the equality method in class \p{BadColoredPoint}.
But then we loose subsumption, the \p{paint} method in class \p{Point}
will fail to type-check. If we want to support both subsumption and
refinement, the only possible solution is to perform a dynamic type test
in the equality method in \p{BadColoredPoint} to check whether the other
given point is colored or not. A restricted form of such a dynamic type
test is performed in languages that support multi-methods (see section
\ref{Sec:RelatedWork}).

The third (and last) possible constraint on the type \p{Self} that can
be specified  is that it will be {\em exactly} the same as the
type of the current class. This type of \p{Self} constraint is required
in some leaf classes of TooL (e.g. Int, Char) that provide builtin
functionality for literal constants (numbers, characters).  It allows
literal constants to be used as return values in methods that are
declared to return a value of type \p{Self}. Such declarations are
usually given in some superclass.

\subsection{Parameterized Classes}
\label{Sec:ClassParameters}

Referring to the example class \p{Set(E)} defined in
section~\ref{xple:set}, we may define a subclass \p{PointSet} that further
constrains the element type to be a subtype of \p{Point} (cf. section
\ref{Sec:Self}). This more specific type information enables us to
access the coordinates of points stored within the set, which can be
used to implement a method that computes the average value of all X
coordinates:
\begin{xple}
  class PointSet(E \subtype Point)
    super Set(E)
    averageX :Int
      {self.inject(0, fun(total :Int, e :E) {total+e.x}) / size}
\end{xple}

As we can see in this example, type parameters of superclasses must be
instantiated explicitly in the subclass. This is the place where a
consistency check is made by the TooL type-checker: the specified actual
type parameter must conform to the bound specified for the formal
parameter, i.e \p{Point} must be a subtype of \p{Object}.

In TooL, type parameters to classes can also be {\em match-bounded} by
some object type. For example, we might define a subclass of
\p{Set} that constrains the element types to match \p{Equality}:
 
\begin{xple}
  class EqualitySet(E \matchtype Equality)
    super Set(E)
    includes(x :E) :Bool
      {elements.some(fun(e :E) {e = x})}
\end{xple}

Here, the more specific constraint on the element type \p{E} enables us
to use the equality test (rather than object identity) for the set
membership test.

Note that our inference rule to obtain subtyping from matching (section
\ref{Sec:SubtypingAndMatching}) is required here in order to ensure that all
types matching \p{Equality} will also be subtypes of
\p{Object}. Otherwise, we cannot ensure type safety by checking the
methods in \p{EqualitySet} in isolation, but we have to type-check
\p{Set} again in the context of the new subclass (where the element type is
bounded differently), losing the modular property of our type
checker.

Although the above example class would also type-check if we had used
subtyping for the bound specification (e.g. \hbox{\p{class EqualitySet(E
\subtype\ Equality)}}), we would not be allowed to instantiate this
class with an element type \p{Point} (cf. section
\ref{Sec:Self}) since \p{Point} is not a subtype of \p{Equality}.
Unfortunately, a similar argument prevents us from instantiating our
\p{EqualitySet} with an element type \p{ColoredPoint} (as defined in
section \ref{Sec:Self}), since \p{ColoredPoint} does not match
\p{Equality}\footnote{Recall that, according to the inheritance rules of
TooL, the type \p{Self} is replaced in superclasses by the corresponding
superclass name iff a subtype-bounded \p{Self} typing is used.}!  This
situation is clearly unsatisfactory. We would like to
instantiate our container class with any type that supports a sufficient
equality operation, which is obviously the case for \p{ColoredPoint}s.

The solution to this problem is a somewhat more complex parameterization
of our container class that combines both subtyping and matching:

\begin{xple}
  class EqualitySet(T \matchtype Equality, E \subtype T)
    super Set(E)
    includes(x :E) :Bool
      \{ elements.some(fun(e :E) {e = x}) \}
\end{xple}

At first glance, this parameterization appears to be unnecessarily
complex, but it intimately reflects our modeling within the inheritance
hierarchy: there is a type \p{T} (\p{Point}) that matches \p{Equality},
and the element type \p{E} (\p{ColoredPoint}) is a subtype thereof.

Currently, the above parameterization evolves as a standard design
pattern within the TooL class library. More complex parameterizations
(such as alternating chains of subtype- and match-bounded type
parameters) do not seem to be necessary. This observation gives rise to
hope that programmers will be able to understand and use the
parameterization with both subtyping and matching, an issue that must be
taken into account when designing a practical programming language.


\subsection{Typing Metaclasses}
\label{Sec:Metaclasses}

Since classes are objects (like any \TooL\ language entity) and every
\TooL\ object is required to be an instance of some class, the need for {\it
metaclasses} arises naturally. While in Smalltalk-80, the metaclass
hierarchy is (implicitly) constrained to parallel (mirror) the normal
class hierarchy, in \TooL\ these two hierarchies are decoupled. This
raises opportunities for powerful reflective meta-programming
\cite{Kiczales91,Briot89,Ferb89,DaFo94}. Not only traditional constructs
that are usually hard-wired into the language (like abstract or virtual
classes, for example), but also more elaborate database functionality
like class extension management and query facilities can be provided
gracefully as a system add-on by defining new metaclasses.

The major problem with metaclass typing is how to type the \p{new}
message that may be sent to an instance of a metaclass (which is a
class), and that returns an instance of the instance of the
metaclass. In Strongtalk, the special keyword \p{Instance} has been
introduced for this purpose. But it has turned out in TooL that the
class parameterization mechanism (section \ref{Sec:ClassParameters}) is
already sufficiently powerful. The idea is to parameterize each
metaclass with the instance type. For example, the metaclass \p{Class}
(which is the default metaclass in TooL) is defined as follows:

\begin{xple}
class Class(Instance \subtype Object)
  super Behavior 
  new :Instance
    \{ $<$builtin "Class new"$>$ \}   ; implementation: a builtin method
\end{xple}

Instances of this metaclass (i.e., ordinary classes) are then typed by
instantiating the \p{Instance} type parameter with the class itself.

\leaveout{
\begin{xple}
Set(E \subtype Object) 
  super Collection(E)
  metaclass Class(Set(E))
\end{xple}


%All classes within the TooL system are stored as pool variables.

The class \p{Set} now has the type \p{Class(Set(E))}.
We have to instantiate the type parameter to \p{Set} before a new
message can be sent to the class:

\begin{xple}
Set(:Int).new
\end{xple}
}


\subsection{Privacy and Encapsulation}

\TooL\ supports the clean separation of the {\em interface specification}
of an object (the set of messages an external client can send to the
object), and the implementation of an object (i.e. the corresponding
method bodies to these messages).  These two parts of an object are
specified in the {\em public} and {\em private} parts of a class
description, respectively. The only object which can legally apply
private methods is the object itself. The expressions where these
methods can be used are restricted to (statically determinable) messages
to the pseudo-variables \p{self} and \p{super}.

Currently, no attempt is made in TooL to provide some extra typing of
the {\em specialization interface} \cite{Lamp93} that is visible to
subclasses of a given class. In TooL, all private methods and slots are
visible within subclasses, i.e. the {\em private} protection level
corresponds to the {\em protected} level of C++.


\section{TooL Implementation Status}

TooL is fully implemented within the Tycoon system infrastructure
developed by our group at Hamburg University during the last four
years. The implementation of TooL itself required six months of work of
the first author (an experienced Tycoon programmer) who developed a
TooL-specific type-checker, a dependency manager for separately compiled
classes, and extensions to the Tycoon runtime system for dynamic method
dispatch.  The efficiency of the current implementation is sufficient
for small to medium-sized programs. Work is in progress to adapt the
Tycoon static and dynamic optimizer to the specific needs of TooL,
incorporating customized compilation \cite{ChUn91,Hoel94,Gawe91a}.

The newly developed fully-fledged polymorphic type-checker implements
structural conformance tests between recursive types using a cache of
already verified conformance relations to detect cycles as described in
\cite{AmCa93}. Furthermore, it utilizes the technique of explicit substitutions
\cite{ACCL90} for lazy polymorphic type variable instantiation.

The TooL parser was built using the Tycoon extensible grammar package
that is based on work described in \cite{CMA94}.
TooL also reuses the Tycoon intermediate code representation \e{TML}
(Tycoon Machine Language), an untyped lambda calculus extended with
imperative constructs that serves as an optimizable, portable program
representation in distributed heterogeneous environments. TML is based
on persistent CPS terms described in \cite{GaMa94,GaMa95},

The TooL runtime system utilizes the
Tycoon Store Protocol which provides a
data-model-independent object store protocol based on the notion of a
\e{persistent heap} that shields TML evaluators (and TooL programmers)
from operational aspects of the underlying persistent store like access
optimization, storage reclamation, concurrency or recovery.  A key
contribution of the TSP to the overall Tycoon system functionality is
support for \e{orthogonal persistence} \cite{AtBu86}: objects and
classes (including code and threads) can exist as long or as short as
required by the application. Programmers do not need to write explicit
code to move data between persistent and volatile store.

Currently, there exist three different TSP implementations that can be 
combined freely with the existing TML evaluators: a compact, paged main 
memory store implementation with a simple file-based persistence mechanism 
\cite{MMS92}; an interface to the Napier persistent object store
\cite{B*91} that  provides an efficient single-user stable store with
recovery mechanisms based on shadow copying exploiting low-level memory
management hardware support; and a gateway to the object-oriented
database system ObjectStore \cite{LLOW92} supporting recoverable
multi-user access to shared databases in client-server architectures.
All store implementations feature automatic garbage collection and
portable data import and export to files.

The Tycoon runtime system is written in C and available on several
hardware and software platforms including SunOS, Solaris, Macintosh,
Linux and Windows.

\section{Related Work}
\label{Sec:RelatedWork}

The common formal interpretation of matching is as a form of F-bounded
subtyping \cite{CCHO89}. Abadi and Cardelli \cite{AbCa95} propose to
interpret matching as higher-order subtyping, arguing that this
interpretation leads to better properties of the matching relation,
e.g. reflexivity and transitivity. The implementation of the matching
relation in TooL conforms to this interpretation. An equivalent
interpretation has been given in \cite{BlHu90}, using a somewhat
different terminology: Black and Hutchinson use the terms {\em namemaps}
(object types) and {\em namemap generators} (type operators).

To our knowledge, Emerald \cite{BlHu90} was the first language
incorporating both subtyping and matching, but it does not support
classes and inheritance. No distinction between ordinary recursion and
self-reference was made.

The languages TOOPLE \cite{Bruc93a} also integrates subtyping and
matching but lacks type rules that relate both notions (see
section~\ref{Sec:SubtypingAndMatching}). PolyTOIL is a recent successor to TOOPLE that adds
polymorphism but is restricted to match-bounded quantification
\cite{Bruc95}. TooL's parameterized classes could be modeled with type
operators in PolyTOIL. However, the interaction between parameterization and
inheritance is not addressed in \cite{Bruc95}.

Strongtalk \cite{BrGr93} aims like TooL to support strong typing in a
pure object-oriented language. Universal type quantification is
provided, but no form of (match or subtype-) bounded quantification is
available.  As discussed in section~\ref{Sec:Metaclasses}, contrary to TooL,
Strongtalk relies on extra typing machinery to type-check metaclasses.
  
In LOOP \cite{ESTZ94}, no destinction between subtyping and matching is
made, attempting to merge the two relations into one, which seems to be
the least common denominator of the two relations.  The subtyping rules
of LOOP are not as powerful as those of TooL and PolyTOIL. While LOOP
does not provide any form of polymorphism, correctness and decidability
have been proved formally.

Multi-methods have been proposed as a solution to the binary method
problem (covariance vs. contravariance) by several authors
\cite{Ghel91,Cast94,Cham92}. Multi-methods circumvent the problem by
choosing an appropriate method implementation on behalf of the dynamic
class or type of {\em every} argument of a message, not merely the
receiver alone. However, multi-methods expose other problems of which
the lack of encapsulation is the most serious one.  Moreover, most
current multi-method approaches identify classes with types again and,
therefore, identify inheritance and subtyping.  Even in Cecil
\cite{ChLe94}, where these problems are addressed (subtype and
inheritance graphs are allowed to differ), an explicit declaration of
subtyping is required.  Therefore, all these models do not scale well
into distributed, open environments where some form of structural
subtyping (or matching) is needed \cite{BlHu90}.

\section{Conclusion}
\label{Sec:Conclusion}

The main contribution of this work is the integration of subtyping, type
matching and type parameterization in an orthogonal language design that
minimizes built-in language functionality in favor of flexible system
add-ons, both at the level of values and at the level of types. The TooL
persistent language is fully implemented and we have reported on our
initial experience in using TooL for pure object-oriented library
construction.

More work remains to be done, like a formal investigation of the
soundness, completeness and expressive power of our type system.  In
this context it is interesting to note that TooL inherits undecidability
from $F_{<:}$ \cite{Pier92} since it employs the same powerful
contravariant subtyping rule on polymorphic functions and methods.
However, during several years of use of the Tycoon language TL we never
ran into problems with (ill-typed) programs that caused our type-checker
to loop endlessly, which we regard as a strong evidence that this
particular form of undecidability is of little practical consequence.

%\newpage

%\bibliographystyle{plain}
\bibliographystyle{enamed}
\bibliography{../bib/agdef,../bib/ag}
%\bibliography{/users/dbis1/matthes/txt/bib/florian-macros,/users/dbis1/matthes/txt/bib/florian}


\end{document}
