Paper announcement on OO type systems

                            PAPER ANNOUNCEMENT

The following short (13 pages long) note


                            Giuseppe Castagna
                Laboratoire d'Informatique de l'ENS, Paris

is available by anonymous ftp at ftp.ens.fr in the file

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)

6. Why all the previous points are strictly related one to each other.



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