[Prev][Next][Index][Thread]

MFPS special session

Date: Thu, 20 Apr 89 17:49:36 -0400
Posted-Date: Thu, 20 Apr 89 17:49:36 -0400

This is a summary description of a special session of MFPS which may
be of interest to some types readers.


  SPECIAL SESSION ON THE SEMANTICS OF INHERITANCE POLYMORPHISM
                 Organized by Carl A. Gunter

A special session was held in conjunction with the New Orleans meeting
of the Conference on Mathematical Foundations of Programming Semantics
on Friday, March 31, 1989.  The purpose of the session was to bring
together researchers who have been working on the development of type
calculi for ``object oriented'' programming languages to discuss
differences of opinion and look for the best directions for future
research.  The session lasted three and a half hours and there were four
speakers:
  Val Breazu-Tannen (Penn)
  John Mitchell (Stanford)
  Atsushi Ohori (Penn)
  Luca Cardelli (DEC)
as well has a substantial period of discussion.  Here is a sort
description of the topics presented by the speakers:

  * Breazu-Tannen outlined the work of himself, Thierry Coquand, Carl
Gunter and Andre Scedrov (BCGS below) which has shown how to interpret
inheritance polymorphism as implicit coercion.  It was emphasized that
this concept is a semantic paradigm which works with many different
calculi and provides a rich supply of models.  A recently formulated
translation technique for inheritance involving the Amber recursion
rule was given.  Cardelli and Mitchell were asked to demonstrate how
their new calculus would deal with a problem of Ohori concerning
``information loss'' which occurs in currently existing calculus for
inheritance.

  * Mitchell discussed his proposal for a type theory for
object-oriented programming constructs such as object, class and
subsumption.  Interestingly, the subsumption that was described cannot
be explained by the Amber recursion rule.  The proposed subsumption
rule therefore provides a new challenge for semantic description.

  * Ohori outlined joint work with Peter Buneman on type inference for
inheritance in ML-like programming langauges and mentioned the
relevance of this research to database applications.  He discussed
their idea of a conditional type scheme as an extension of ML
principal type schemes and outlined a proposal for classes and
inheritance in this famework.  From this work and that of others, it
appears that an extension of ML that includes inheritance may now be
possible.  There was a discussion of the relationship between this
work and the work of Jategaonkar and Mitchell.

  * Cardelli discussed tradeoffs between two proposed forms of
semantics for inheritance:
    SUBSUMPTION SEMANTICS
    COERCION SEMANTICS
He argued that the former semantic technique offers to throw light on
basic issues involving the implementation of inheritance in which
SUBTYPES are intuitively SUBSETS.  The BCGS coercion semantics does
nothing to explain this intuition and does not suggest a reasonable
technique of implementation.  It was counter-argued (by certain
parties in the audience) that the BCGS semantics can be seen as a
specification and need not be associated with any particular
implementation idea.  There was also a lively discussion of the
limitations of coercion semantics for language constructs which can
branch on the form of a type; Peter Freyd and John Reynolds argued
that such constructs violate uniformity and constitute ad hoc
polymorphism.


Following these presentations there was a period of short impromptu
presentations.  Breazu-Tannen presented an important semantic issue
concerning the meaning of inheritance coercions.  Such maps must be
stict if the desired coherence properties are expected to hold.  It
was noted that coercion maps are also total.  Cardelli proposed the
question of whether the coercion maps obtained from the BCGS
translation might be uniquely determined by an appropriate list of
such semantic conditions together with the coherence requirement.

Cardelli showed how the new Mitchell/Cardelli calculus could handle
the question proposed by Breazu-Tannen in the first presentation.
John Mitchell offered to collect examples generated by the session
via net mail, so we would be able to keep some record.

John Reynolds suggested that many of the objectives of researchers
currently working on inheritance (including the ones at this session)
could be solved by the use of the conjunctive types of Coppo and Dezani.
There was some discussion of the limitations of conjunctive types.
At least two questions were asked:
(1) Can conjunctive types be integrated with parametric polymorphism?
(2) Is there a way to represent ``record update'' in a calculus with
conjunctive types?
Answers to these questions seem critical if conjunctive types are to
fully deal with issues discussed in the session.