# 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

-------------

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
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