[Prev][Next][Index][Thread]
Paper announcement on OO type systems
PAPER ANNOUNCEMENT
==================
The following short (13 pages long) note
"COVARIANCE AND CONTRAVARIANCE: CONFLICT WITHOUT A CAUSE"
Giuseppe Castagna
Laboratoire d'Informatique de l'ENS, Paris
is available by anonymous ftp at ftp.ens.fr in the file
/pub/reports/liens/liens-94-18.A4.dvi.Z
ADVERTISEMENT: This paper tries to explain
-------------
1. What covariance and contravariance serve for.
2. Why covariance and contravariance are not opposing views but both
*must* be integrated in a *type-safe* formalism. I.e.: don't choose
just one of them.
3. Where the "objects as records" analogy hides covariance.
4. How to type binary methods in the models based on the analogy "objects
as records" (i.e. how to have ColorPoint < Point even if they respond
to a message "equal")
5. How to have multiple dispatch when objects are modeled by (recursive)
records.
6. Why all the previous points are strictly related one to each other.
ABSTRACT
In type theoretic research on object-oriented programming the ``covariance
versus contravariance issue'' is a topic of continuing debate. In this
short note we argue that covariance and contravariance appropriately
characterize two distinct and independent mechanisms. The so-called
contravariance rule correctly captures the {\em substitutivity\/}, or
subtyping relation (that establishes which sets of codes can replace {\em
in every context\/} another given set). A covariant relation, instead,
characterizes the {\em specialization\/} of code (i.e.\ the definition of
new code that replaces the old one {\em in some particular cases\/}).
Therefore, covariance and contravariance are not opposing views, but
distinct concepts that each have their place in object-oriented systems
and that both can (and should) be type safely integrated in an
object-oriented language.
We also show that the independence of the two mechanisms is not
characteristic of a particular model but is valid in general, since
covariant specialization is present also in record-based models, but is
hidden by a deficiency of all calculi that realize this model.
As an aside, we show that the lambda&-calculus can be taken as the basic
calculus both for an overloading-based and for a record-based model. In
that case, one not only obtains a more uniform vision of object-oriented
type theories but, in the case of the record-based approach, one also
gains multiple dispatching, which is not captured by the existing
record-based models.
Giuseppe Castagna
------------------------------------------------------------
LIENS (CNRS) Tel. ++33-1-4432 2082
Ecole Normale Superieure FAX. ++33-1-4432 2080
45, rue d'Ulm
75005 Paris castagna@dmi.ens.fr