% File: ecoop96.tex
% Author: Gawecki, Matthes
% Purpose: ECOOP'96
% Date: 19-Mar-1996 (Final Version)
%
\documentstyle[snamed,ecoop96,epsf]{llncs}

\title{\parbox{12.5cm}{{\footnotesize\vspace*{-1cm}Appeared in: \e{Proceedings of the 10th European Conference on Object-Oriented Programming, ECOOP'96}, Linz, Austria, July 1996. Springer Verlag.}}\\
$ $\\
Integrating Subtyping, Matching 
and Type Quantification:\\ A Practical Perspective\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).
}}

\author{Andreas Gawecki \quad Florian Matthes}

\institute{
Universit\"at Hamburg, Vogt-K\"olln-Stra{\ss}e 30 \\
D-22527 Hamburg, Germany \\
%Phone: +49 40 54715 332\\
%Fax: +49 40 54715 328\\
\{gawecki,matthes\}@informatik.uni-hamburg.de}
 
\sloppy
\frenchspacing

\begin{document}

\parskip 1.5ex
\parindent 0ex

\maketitle

\begin{abstract} \noindent We report on our experience gained in designing,
implementing and using a strongly-typed persistent programming language (TooL)
which integrates object types, subtyping, type matching, and type
quantification. Our work complements recent type-theoretical studies of subtyping
and type matching by focusing on the issue of how to integrate both concepts
into a practical, orthogonal programming language. We also shed some light on
the subtle typing issues which we encountered during the construction of a
substantial bulk data library where it was necessary to trade-off subtyping
against type matching. Our practical experience suggests that the benefits of
an integration of subtyping and type matching are achieved at the expense
of a significant increase in modeling complexity.
\end{abstract}

\newpage

\section{Introduction and Motivation}

The purpose of this paper is to report on our practical experience gained in
designing, implementing, and using \k{TooL}, a language integrating subtyping
and type matching, which should be of value for anyone who plans to incorporate
type matching into a fully-fledged programming language.

The TooL project started off with the observation that existing
statically-typed polymorphic programming languages with subtyping only
(Modula-3 \cite{Nels91}, C++ \cite{ElSt90}, Tycoon \cite{MaSc92a} or Fibonacci
\cite{AGO94}) provide application programmers with rich re-usable generic class
libraries organized into subtype hierarchies. However, the type system of these
languages obstructs programmers who intend to maximize code sharing between
library classes through implementation inheritance following the successful
library design principles of Smalltalk and Eiffel. As discussed in the
literature \cite{BlHu90,Bruc94,Bruc95a,AbCa95} and illustrated in the rest of
the paper, a more liberal notion of \e{type matching} is needed, for example,
to support the type-safe inheritance of \e{binary methods} \cite{BCC*95}.

The design and implementation of TooL has been heavily influenced by experience
gained with the \k{Tycoon} language \cite{MaSc92a} developed at the University
of Hamburg in the framework of the European basic research project FIDE
\cite{Atki96} where six European database language research groups collaborated
towards the goal of \e{Fully Integrated Data Environments} using
state-of-the-art language technology.

The rationale behind the original Tycoon type system is to provide a set of
unbiased, orthogonal primitives to support various database programming styles,
including 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{Card89,CaLo91} and the type
theoretic model of $F_{<:}^{\omega}$ \cite{PiTu93b}.

Based on our extensive experience using Tycoon for large-scale programming (for
example, building and maintaining systems with several hundred modules) our
motivation behind the design of TooL was to verify the following hypotheses:
(1) A \e{purely} object-oriented language where objects and classes combine
aggregation, encapsulation, recursion, parameterization and inheritance leads
to program libraries which are more uniform and easier to understand since
programmers do not have the freedom to choose between combinations of modules,
records, tuples, functions, recursive declarations, etc.  (2) Type matching
increases code reuse within complex libraries.

To verify these hypotheses it was not only necessary to design and to implement
TooL, but also to \e{utilize} it for non-trivial library examples.  In a
nutshell, this experimental validation was carried out by augmenting the Tycoon
type system by a notion of type matching, omitting existential type
quantification and all higher-order type concepts like kinds, but otherwise
adhering closely to the proven type and language concepts of Tycoon.  We then
used the functionality of the mature and highly-structured Eiffel collection
library \cite{Meyer90} as a yardstick for the construction of a type-safe TooL
bulk type library.

This paper is organized as follows: In section~\ref{Sec:Rationale} we provide
insight into the rationale behind the TooL language
design. Section~\ref{Sec:AST} and section ~\ref{Sec:Library} as well as the
appendix give an overview of the language and the libraries constructed with
the language.  Section~\ref{Sec:TypeConcepts} motivates and explains the TooL
subtyping, matching and type quantification rules. The TooL inheritance rules
and the non-trivial interaction of subtyping, matching and type quantification
are discussed in section~\ref{Sec:Inheritance} and section
\ref{Sec:SubtypingAndMatching}, respectively. The impact of this
interaction on the use of the TooL language for library programming is
described in section~\ref{Sec:Experience}. The paper ends with a comparison
with related work and a summary of our research contributions.


\section{TooL Design Goals}
\label{Sec:Rationale}

The key aspects of the TooL language design can be summarized as follows:

\begin{description}

\item[Purely object-oriented:] \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{purely} 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 such as integer arithmetic, variable access, and array
indexing are uniformly expressed by sending messages to objects.

It should be noted that modern compiler technology eliminates most of the
run-time performance overhead traditionally associated with the purely
object-oriented approach \cite{ChUn91,Hoel94,Gawe92a}. For example, TooL uses
dynamic optimization across abstraction barriers based on a persistent
continuation passing style (CPS) program representation to ``compile away''
many message sends \cite{GaMa96a}.

\item[Higher-order functions as objects:] Contrary to other statically-typed
object-oriented languages \cite{Gogu90}, TooL provides statically-scoped
higher-order functions which are viewed as first-class objects that
understand messages. Thereby control structures like loops and conditionals 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 instance and
pool variables (which unify the concepts of global and class variables in
Smalltalk) are accessed by sending messages \cite{JoFo88}. This unification 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.

\item[Strong and static typing:] No operation will ever be invoked on an 
object which does not support it, i.e.  errors like ``message not 
understood'' cannot occur at run time.  Type rules are defined in a 
``natural-deduction'' style based on the abstract TooL syntax similar to 
\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.

\item[Structural type checking:] 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.

\item[Modular type checking:] During type checking of a given class
only the interfaces of imported classes and of superclasses have to be
accessed. 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 is in conflict with substitutability. Therefore,
Eiffel requires some form of global data flow analysis at
link-time to ensure type correctness. Such an analysis generally requires a
representation of the source code of all classes and methods which
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}

\section{TooL Syntax Overview}
\label{Sec:AST}

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. This semantic
simplicity and orthogonality is reflected by the abstract syntax of TooL
depicted in figure~\ref{Fig:AST} which provides a starting point for the
definition of the static semantics of TooL and which constitutes the canonical
internal representation used by the TooL language processors.

\begin{figure}\small
\begin{center}
\begin{tabular}{rll}
$\psi::=$&   $\subtype$   	 & subtyping \\
    $|$ & $\matchtype$    & type matching \\
    $|$ & $\equals$        & type equivalence \\
$S::=$  & $\emptysig$ & empty signature \\
    $|$ & $S,x \hastype T$ & value signature \\
    $|$ & $S,X \psi T$ & type signature \\
$D::=$  & $\emptybind$ & empty binding \\
    $|$ & $D,x \equals v$ & value binding \\
    $|$ & $D,x \hastype T \equals v$ & constrained value binding \\
    $|$ & $D,X \equals T$ & type binding \\
$T::=$  & $\k{Nil}$ & bottom type constant \\
    $|$ & $A$ & type identifier or type instantiation \\
    $|$ & $\Interface{X}{S}{Self}{} $ & named parameterized object type\\
	& $\quad \{m_1(S_1)T_1,\dots,m_n(S_n)T_n\}$ & \\
$A::=$  & $X$		 & type identifier\\
    $|$ & $X(D)$	 & type instantiation (type bindings only)\\
$v::=$&   $b$   	 & constants (integer, character, \ldots literals)\\
    $|$ & $\k{self}$ $|$ \k{super}     & receiver object \\
    $|$ & $x$		 & value identifier\\
    $|$ & $\k{fun}(S)D$  & (polymorphic) function constructor\\
    $|$ & $\send{m}{v}{D}$ & message send \\
$c::=$  & $Self \; \psi\ \; \k{class}\; X(S;A_1,\dots,A_n;A)$ & named class definition   \\
	& $\quad \k{public} \; slots \; methods$ \\
	& $\quad \k{private} \; slots \; methods$ \\
$slots::=  $  &  $x_1 \hastype T_1, \dots,x_n \hastype T_n$ &  \\
$methods::=$  &  $m_1(S_1)T_1 \equals D_1, \dots,m_n(S_n)T_n \equals D_n$ &  \\
\end{tabular}
\end{center}
\caption{The TooL abstract syntax}
\label{Fig:AST}
\end{figure}

The definition of the abstract TooL syntax involves syntactic objects that are
denoted by meta variables using the following naming conventions:
\begin{center}\small
\begin{tabular}{ll}
$X,Y,Self$ &  type and class identifiers \\
$x,y$ & value identifiers \\
$\psi$   & type relations  \\
$S$   & type and value signatures \\
$D$   & type and value bindings \\
$T$   & type expressions \\
$A$   & named type expressions \\
$v$   & values \\
$m$   & method selectors \\
$c$   & named class definitions \\
$slots$   & instance variable declarations \\
$methods$   & method declarations \\
\end{tabular}
\end{center}
Since most aspects of the abstract syntax are similar to other
polymorphically-typed languages \cite{CaLo91,Card93}, we only highlight 
some of the productions.

A TooL program is a set of (mutually recursive) named class definitions
$c_1,\ldots, c_n$.

A class definition defines the name of the $Self$ type (see
section~\ref{Sec:Matching}), the name $X$ of the class, the signatures $S$ of
the class type parameters, an ordered sequence of direct superclasses
$A_1,\dots,A_n$, a metaclass declaration $A$ (not treated in this paper), and a
set of public and private slots and a suite of method declarations. Each method
declaration specifies a method selector $m_i$, the signatures $S_i$ of the
method arguments, the method result type $T_i$, and a method body $D_i$ given
by a list of bindings. The return value computed by a method is the value of
its last value binding.  A class declaration implicitly defines an object type
$\Interface{X}{S}{Self}{} \{m_1(S_1)T_1,\dots,m_n(S_n)T_n\}$ with the same
name.

A message send operation defines a message $m$ which is sent to an object
determined by evaluating the receiver expression $v$, passing a sequence $D$ of
type and value bindings as actual parameters.

Within bindings and signatures, a distinguished \e{anonymous} identifier '\_'
can be used to denote omitted identifiers. For example, the expression
\p{x.m(3)} in the concrete syntax is mapped to the binding
$\_=\k{send}(m,x,(\emptybind, \_=3))$.

A function type (denoted as \p{\k{Fun}(S):T} in the concrete syntax of our 
examples) is represented as an object type with an apply method with 
signature $S$ and result type $T$. A function abstraction $\k{fun}(S)D$ 
evaluates to an instance of such an object type.

Each slot $x:T$ is mapped to a pair of an access method and an update method
with the signatures $x_{get}(\emptysig):T$ and $x_{set}(\emptysig, \_
:T):\k{Void}$, respectively.

\TooL\ supports a separation of classes into a {\em
public} and a {\em private} part. 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}.

Despite the semantic simplicity of TooL, a rich set of syntactic
variants exists 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. In fact, the TooL language is based on
extensible grammars \cite{CMA94} which give users full control over the
concrete syntax of TooL, for example, to support domain-specific abstractions
like query language notations or concurrency control schemes. The default
concrete syntax used in this paper is similar to C++ and Java.

\section{The TooL Bulk Type Library}
\label{Sec:Library}

Figure~\ref{Fig:TooLLibrary} shows the part of the TooL class library relevant
for bulk data manipulation. A bold font indicates concrete (instantiable)
classes, whereas a non-bold font indicates abstract classes, i.e., classes
where some or all method bodies consist of empty bindings (cf.~figure~\ref{Fig:AST}).

\begin{figure}[btp]
\epsfbild{container.eps}{\epsfxsize=\columnwidth}
\caption{Overview of the TooL bulk type library}
\label{Fig:TooLLibrary}
\end{figure}

This class hierarchy is designed to maximize code sharing between library
classes through implementation inheritance following the successful library
design principles of Smalltalk and Eiffel \cite{Meyer90}. For example, the
abstract classes \p{Boxed}, \p{Accessible}, and \p{Traversable} provide code
fragments which capture certain aspects of containers and which can be
inherited, combined and refined in subclasses to implement concrete classes
such as priority queues.

In the rest of the paper, we will utilize this library not only to explain some
of the more subtle TooL language design decisions, but also to shed some light
on the practical issues that arise if subtyping, type matching
and type quantification interact.


\section{Basic TooL Type Concepts}
\label{Sec:TypeConcepts}

In this section we motivate and explain the TooL subtyping, matching and type
quantification rules. Their impact on the TooL inheritance rules and their
non-trivial interaction is discussed in later sections.

\subsection{Structural Subtyping}

The main motivation for 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:Quantification}.

As a practical example for substitutability in the TooL libraries, consider the
\p{printOn} method defined in class \p{Object} to print any TooL object onto a
stream of characters:
\begin{xple}
\k{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 \p{File}.
\begin{xple}  
"a string".printOn(stdout)
\end{xple}
In order to substitute a \p{File} in a context where a \p{WriteStream} of
characters is expected, we have to show the subtype relationship
\hbox{\p{File \subtype\ WriteStream(Char)}}.

Note that 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}
\k{class} WriteStream(E \subtype Object)
  put(e :E) :Void 

\k{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}
which is bounded by the type \p{Object} (cf. section \ref{Sec:Quantification})
and exports a single method \p{put} to append an object \p{e} of type \p{E} to
the stream.  The (possibly independently defined) unparameterized class
\p{File} also exports a \p{put} method, which only accepts characters, in
addition to a \p{get} 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.
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{Bruc95a}). 

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} which 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. At runtime, however, only the
methods defined in class \p{Nil} and its single superclass \p{Object}
(e.g. identity testing and printing) may be legally applied, sending any other
message to \p{nil} triggers an exception. The value \p{nil} is used to
initialize instance variables and to mark empty slots in hash tables. The type
\p{Nil} is also used to type expressions which raise an exception.

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

As explained in the introduction, a key contribution of TooL is to provide a
second relation between object types in addition to subtyping. This relation is
called {\it matching} (denoted by \p{A \matchtype\ B}) and has been introduced
in type-theory \cite{BlHu90,Bruc94} 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 binary
methods as a special case.

Intuitively, the matching relation captures certain forms of 
self-referential similarity of object types.  Similar to \p{MyType} in 
PolyTOIL \cite{Bruc95a} or \p{like Current} in Eiffel, a distinguished type 
identifier \p{Self} is used in TooL to indicate a self reference which is 
automatically updated during subclassing to refer to the new subclass.

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

In the following example, we define a class \p{Equality}
supporting a single infix equality predicate (\p{"="}):
\begin{xple}
\k{class} Equality
  "="(x :Self) :Bool
\end{xple}
Exploiting the notion of matching in TooL we can write a generic method
\p{"!="} which compares two objects for equality and returns the negated
result. All that is required is to know that both objects are of some type
\p{T} which 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 which \e{match} the type \p{Equality}, like the
following class \p{Int} which exports two additional binary infix
operators:
\begin{xple}
\k{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}. 

As explained in section~\ref{Sec:Inheritance}, the explicit type quantification
in the definition of the method \p{"!="} can be 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}
\k{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{Type Quantification}
\label{Sec:Quantification}

Classes as discussed up to now introduce named type constants.  Classes can 
be turned into {\em generic classes} by type parameterization.  Type 
parameterization is important for the type-safe definition of generic 
container classes and polymorphic iteration abstractions.  For example, 
virtually all subclasses of \p{Container} (see figure~\ref{Fig:TooLLibrary})
have one or several formal type parameters.

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}
\k{class} Set(E \subtype Object)
  add(e :E) :Void
  includes(e :E) :Bool
  inject(F \subtype Object, unit :F, f :\k{Fun}(:F, :E):F) :F
  map(F \subtype Object, f :\k{Fun}(:E):F) :Set(F)
  printOn(aStream :WriteStream(Char))
\end{xple}
This class interface shows that type parameterization is also available in
individual method and function signatures, for instance in the higher-order
\p{inject} method which 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}.

In TooL, parameterized classes are not simple templates which can only be
type-checked after instantiation as in C++ or in Trellis. Type parameters are
{\em bounded} by a type, permitting local, modular type checking within the
scope of the quantifier. For example, the element type of the set returned by
the polymorphic \p{map} method depends on the argument type of the function
\p{f} passed as a run-time argument to the \p{map} function.

As indicated by 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, thus \p{intSet.inject(0, plus)} is equivalent to
\p{intSet.inject(:Int, 0, plus)}.  This is particularly useful in the typing of
control structures modeled with message passing.  We use a simple but
incomplete inference algorithm similar to the one described in \cite{Card93}
which works well in practice.

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


\section{Inheritance}
\label{Sec:Inheritance}

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 which can be reused and modified by multiple
inheritance. This is one of the main differences between TooL and Tycoon.

Similar to CLOS \cite{BDG*88}, a TooL class
definition may give an ordered specification of its direct superclasses, for
example the container class \p{Indexed} with an element
type \p{E} inherits from two superclasses
(see figure~\ref{Fig:TooLLibrary}):
\begin{xple}
\k{class} Indexed(E \matchtype Equality)
\k{super} Bounded(E), Keyed(Int, E)
\end{xple}
Possible inheritance conflicts (name clashes between inherited methods) 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}. More
elaborated schemes of conflict resolution are possible, for example allocating
different roles for objects as in Fibonacci \cite{AGO94}. We chose to omit
such sophisticated features to keep our language simple and to focus on the
typing issues discussed in the subsequent sections.

If a method specification \p{m(S):T} takes precedence during method lookup
over another method specification \p{m(S'):T'}, the result type \p{T} has to be
a subtype of \p{T'} assuming that the signatures \p{S`} are subsignatures of
the signatures \p{S}. The full type rules for inheritance in TooL are similar
to those of PolyTOIL \cite{Bruc95a} and have to take parameterized classes and
Self type specifications (see section~\ref{Sec:Self}) into account.

Type parameters of superclasses may be refined during inheritance.  For 
example, a subclass \p{PointSet} can be defined which further constrains 
the element type of class \p{Set} to be a subtype of \p{Point}.  This more 
specific type information enables us to access the coordinates of points 
stored within the set to compute the average value of all \p{X} 
coordinates:
\begin{xple}
\k{class} PointSet(E \subtype Point)
\k{super} Set(E)
  averageX() :Int \{\k{self}.inject(0, \k{fun}(total :Int, e :E) {total+e.x}) / size\}
\end{xple}
In this example, a consistency check is performed by the TooL type-checker to
verify that the specified actual type parameter conforms to the bound specified
for the formal parameter, i.e \p{Point} has to be a subtype of \p{Object}.

\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}. Due to subclassing, this assumption must take {\em
all} possible extensions of $c$ into account since we want to perform modular
type-checking. As described in this section, a major contribution of TooL is to
give the library programmer explicit control over this particular assumption.

In the most commonly used object-oriented languages (e.g. C++, ObjectPascal,
Modula-3, Eiffel), subclassing means subtyping. In these languages,
\p{Self} has to 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{Bruc94}, PolyTOIL
\cite{Bruc95a}), the subtype hierarchy implicitly defined by the subtype
relation '$\subtype$' does not have to be the same as the class hierarchy
explicitly defined by inheritance declarations: class specialization by
inheritance can lead to {\em incompatible} types which are not related by
subtyping any more. In these languages, inheritance ensures {\em matching} of
subclasses. This means that the only assumption that can be made during modular
type-checking is that \p{Self} will always match the current class.  This {\em
match-bounded} \p{Self} typing provides more flexibility because the programmer
is not constrained to produce subtypes during subclassing.

Finally, there are programming situations where library designers would like to
express the constraint that all subclasses will have identical types and only
differ in their method implementations. For example, the TooL leaf classes
(\p{Int}, \p{Char}, \ldots) which provide builtin functionality for literal
constants (numbers, characters, \ldots) require this constraint to allow
literal constants to appear as return values in methods with return type
\p{Self}.

Therefore, TooL offers three kinds of \p{Self} typing (subtype-bounded,
match-bounded and equivalence), leaving the choice to the programmer to use one
of the following notations:
\begin{xple}
\k{class} Equality \ldots
Self \matchtype\ \k{class} Equality \ldots
Self \subtype\ \k{class} Equality \ldots
Self = \k{class} Equality \ldots
\end{xple}
The notation \p{class Equality \ldots} is a shorthand for \p{Self \matchtype\
class Equality \ldots}. We now discuss the advantages and disadvantages
of theses alternatives in turn.

In general, match-bounded \p{Self} typing is used in classes close to the root
of the inheritance lattice to support inheritance of methods with contravariant
occurrences of \p{Self}, e.g. binary methods.  A switch to subtype-bounded
\p{Self} typing can then be performed when going down the inheritance lattice
to support subsumption.

For example, 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 class \p{Equality}, but we
override the default implementation of equality which uses simple object identity:
\begin{xple}
Self \matchtype\ \k{class} Equality
  \k{super} Object
  "="(x :Self) :Bool \{ self == x \}
  "!="(x :Self) :Bool \{ !(self = x) \}
  
Self \subtype\ \k{class} Point
  \k{super} Equality
  x :Int
  y :Int
  "="(aPoint :Self) :Bool \{ x = aPoint.x \& y = aPoint.y \}
  paint(aPen :Pen) :Void  \{ aPen.dot(self) \}
    
Self \subtype\ \k{class} ColoredPoint
  \k{super} Point
  color :Color
  $\ldots$
\end{xple}

In the classes \p{Point} and \p{ColoredPoint}, we have explicitly specified
which assumption the type-checker should make about \p{Self}, 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 which
expects a \p{Point} as an argument, e.g. the
\p{dot} method of \p{Pen}.

\subsection{Enforcing the Self Constraint}

A \p{Self} constraint assumed during modular type checking is enforced when actual
subclassing takes place:

\begin{enumerate}

\item Inheritance from a match-bounded class \p{Self \matchtype \k{class} c} is
equivalent to copying the method signatures of \p{c} into the subclass.

For example, the match-bounded \p{Self} in class \p{Equality} above makes it
possible to overwrite the equality method with contravariant occurrences of
\p{Self} in the subclass \p{Point}, producing a subclass which is not a
subtype of \p{Equality}.

\item Inheritance from a subtype-bounded class \p{Self \subtype \k{class} c}
is equivalent to copying the method signatures of \p{c} into the subclass and
replacing all inherited occurrences of \p{Self} by \p{c}, turning all explicit
self references into implicit ones. Therefore, subclasses do not have to
match \p{c} any more. For 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).

At 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 specialized automatically in subclasses.
However, this approach is unsound if we do not treat positive
(covariant) and negative occurrences of \p{Self} as different types.
From our practical experience we believe that the additional
complexity of introducing two distinct Self type variables is not worth the
relatively small gain in expressive power.

As a consequence of the subtype constraint, 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} in
the following way, trying to take the color attribute into account during the
comparison:

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

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

Note that a match-bound \p{Self} specification for class \p{Point} would enable
a further refinement of the equality method in class \p{BadColoredPoint}.  But
then subsumption on \p{self} would be lost and the \p{paint} method in class
\p{Point} would fail to type-check.

More general, to support \e{both} subsumption and refinement in TooL, a dynamic
type test in the equality method in \p{BadColoredPoint} is required to check
whether the argument is colored or not. A restricted form of such a dynamic
type test is performed in languages which support multi-methods (see section
\ref{Sec:RelatedWork}).

\item Inheritance from a  class \p{Self = \k{class} C} is equivalent to (1) and
requires a check that no additional methods are defined or refined in the subclass.

\end{enumerate}

In all three cases inheritance implies code sharing.

\section{Reconciling Subtyping, Matching and Quantification}
\label{Sec:SubtypingAndMatching}

Up to now, we have 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 important to have expressive type rules which establish 
relationships between elements in the subtyping and matching lattice.

The following \TooL\ type rule states 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.

Intuitively, this rule is sound because matching requires that $X$ must contain
at least the methods present in the method suite $M$, and if
$\hbox{ObjectType}(Self)M[X/Self]$ is a subtype of $T$, $X$ must also contain
at least the methods present in $T$ (due to reflexivity of subtyping).  This
means that, by the definition of matching (see also \cite{AbCa95,Bruc95a}), $X$
can only be not a subtype of $T$ if $M$ contains methods with negative
(contravariant) occurrences of \p{Self}. But this case is covered since these
have been replaced by $X$.

While it seems possible to map all other TooL type rules (not shown in this
paper) in a rather straightforward way onto corresponding type rules of core
languages developed for the formal study of type systems incorporating some
form of matching, this particular rule indeed looks rather ``ad-hoc'' and
suspicious to a type theoretician. Without this rule, many of TooL class
definitions would not type-check successfully. From a type-theoretical point of
view it should therefore be interesting to formally prove the soundness of
this rule or to come up with an equivalent or a more general rule, which might
be easier to prove.

This TooL type rule is utilized, for example, to prove the trivial
relationship \p{X \subtype Void} for any type variable \p{X} which is known to
match some object type.  Otherwise, special inference rules involving the top
type \p{Void} have to be added to the type system (as, for example, in PolyTOIL
\cite{Bruc95a}).

Bounded type parameterization leads to other, more compelling practical
examples where the type rule {\it [Match vs. Subtype]} is needed.  For example,
we might define a subclass of \p{Set} by inheritance which further constrains
the set element types to match \p{Equality}, overriding the element constraint
\p{E\subtype Object} (see section~\ref{xple:set}):
\begin{xple}
\k{class} EqualitySet(E \matchtype Equality) \k{super} Set(E) 
  includes(x :E):Bool \{elements.some(\k{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. The type rule {\it [Match vs. Subtype]} ensures that all types matching
\p{Equality} will also be subtypes of \p{Object}. Without this rule we could
not ensure type safety by checking the methods in \p{EqualitySet} in isolation,
but we would have to type-check \p{Set} again in the context of the new
subclass (where the element type is bounded differently), violating our design
principle of modular type checking.

Unfortunately, the type 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 larger 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.

For practical programming in TooL, the lack of a rule to deduce matching from
subtyping is a major problem in library construction, since it is not ``safe''
to simply replace matching by the ``stronger'' subtyping constraint wherever it
holds between any two classes.

\section{Programming Experience}
\label{Sec:Experience}

In this section we try to assess the impact of the increased type system
expressiveness gained by the introduction of matching on the practical value 
of the TooL language.

First, subtyping and type matching both interact well with other TooL 
language concepts such as type quantification and Self type constraints.  
Moreover, students with some background in strongly-typed higher-order 
programming languages like Modula-3 or Tycoon grasp these concepts rather 
fast.  However, as already discussed in section~\ref{xple:BadColored} and 
\ref{Sec:SubtypingAndMatching}, problems arise as soon as programmers wish 
to combine the advantages of both partial orders on types.

For example, library designers typically prefer match-bounded quantification
to maximize code reuse. This may conflict with the goal of library clients
which like to exploit the subsumption property of subtyping to absorb later
(unforseen) system extensions. As a concrete example, consider a method \p{f} in an
application class with the following signature:
\begin{xple}
 f(d :Dictionary \ldots) \ldots
\end{xple}
This method can be applied uniformly to all instances of classes \p{D} derived
by subtyping from the class \p{Dictionary}. To achieve the same effect for all
classes \p{D} matching \p{Dictionary}, a verbose explicit match-bounded
quantification has to be used in all application methods which is 
unlikely to be carried out in practice:
\begin{xple}
 f(D \matchtype Dictionary d :D \ldots) \ldots
\end{xple}

A similar argument holds for type parameters of classes. For example, the
constraint \p{E \matchtype Equality} for the class \p{EqualitySet} defined in
the previous section works fine only if we refrain from deriving subclasses by
subtyping. If we attempt to instantiate \p{EqualitySet} with type
\p{ColoredPoint}, the type checker would fail to verify \p{ColoredPoint
\matchtype Equality} since the type \p{Self} in class \p{ColoredPoint} is
replaced by \p{Point} during subtype-bounded inheritance.

Again, a more elaborate parameterization would solve
this problem:
\begin{xple}
\k{class} EqualitySet2(T \matchtype Equality, E \subtype T)
\k{super} Set(E)
  includes(x :E) :Bool \{ elements.some(\k{fun}(e :E) \{e = x\}) \}
\end{xple}

More complex parameterizations (such as alternating chains of subtype- and
match-bounded type parameters) do not seem to be necessary. Up to now, we have
found no compelling example where a subclass of a subtype-bounded class needs
to be refined by match-bounded inheritance.

Since such investigations can only be carried out by implementing practical
programming languages and by using them for application development, the 
TooL experiment constitutes a valid complement to ongoing 
type-theoretical research on the integration of type matching and 
subtyping.

\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{Bruc94} also integrates subtyping and
matching but lacks type rules which relates one notion to the other (see
section~\ref{Sec:SubtypingAndMatching}). PolyTOIL is a recent
successor to TOOPLE that adds
polymorphism but is restricted to match-bounded quantification
\cite{Bruc95a}. The parameterized classes of TooL could be modeled with type
operators in PolyTOIL. However, the interaction between parameterization and
inheritance is not addressed in \cite{Bruc95a}.

Like TooL, Strongtalk \cite{BrGr93} aims to support strong typing in a purely
object-oriented language. Universal type quantification is provided, but no
form of (match or subtype-) bounded quantification is available.  Contrary to
TooL, Strongtalk relies on extra typing machinery to type-check metaclasses.
  
In LOOP \cite{ESTZ94}, no distinction 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 bounded
type quantification, 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 results of our work presented in this paper can be summarized as
follows:

Type matching and subtyping can be integrated orthogonally and cleanly into a
fully-fledged, practical programming language based on a rather small set of
constructs at the type and at the value level. In particular, type matching
interacts well with type quantification.

In a type system with subtyping and matching, modular type checking requires
the programmer to specify how the receiver type \p{Self} is related to the type
of the enclosing class. TooL offers three possibilities: (1) \p{Self} is a
subtype of the enclosing class; (2) \p{Self} matches the enclosing class; (3)
\p{Self} is identical to the enclosing class.

Existing type-theoretical models of languages incorporating subtyping and type
matching lack type rules to derive relationships between elements in the
subtype and the matching lattice which are important for library
construction. We define and informally justify such a type rule for
TooL. Together with the presentation of the TooL core syntax we thus provide
useful input for further type-theoretical work in this area. In this context it
is interesting to note that TooL inherits undecidability from $F_{<:}$
\cite{Pier94} since it employs the same powerful contravariant subtyping rule
on polymorphic functions (i.e. methods). However, this contravariant rule could
be replaced by a more rigid rule which avoids undecidability without
invalidating any of the existing TooL library classes.

A comparison of the TooL class library with the Tycoon bulk type library
supports both our hypotheses stated in the introduction of this paper: TooL as
a purely object-oriented language with type matching leads to more uniform
program libraries with an increased code reuse. However, we also observed some
practical difficulties encountered by programmers designing
large libraries involving both matching and subtyping.

{\small

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

}

\end{document}


