[Prev][Next][Index][Thread]
Re: bounded quantification and record-update problems
Date: Thu, 20 Oct 88 09:35:06 EDT
To: rdt%QUCIS.BITNET@mitvma.mit.edu, types@theory.LCS.MIT.EDU
A note on Tennant and Robinson's remarks on the Bruce-Longo model. Mitchell
raised similar questions last spring, and in fact we worked out the Lemma
in Tennant and Robinson's remarks at the Semantics and Category theory
conference at CMU in the spring (unfortunately too late to get into the LICS
proceedings). As Jategaonkar and Mitchell point out in the last paragraph
of their paper in this summer's LISP conference, the Bruce-Longo model has
"too many" types. That is, since every subset of a type is a type, all single
element subsets are subtypes, leading to the proof of the lemma. Thus the
idea is to provide a model with the subtypes generated by records, but not
by all possible subsets. (The more I have thought about this, the more
convinced I have become that subset or subranges of types ought not to be
considered subtypes, both because of problems like the above, but perhaps
more compellingly, by the difference between what is statically typeable and
what must be checked dynamically - decideable vs undecideable, etc.).
I still believe that the structure of the Bruce-Longo model is more
satisfactory than the one proposed by Breazu-Tannen, Gunter, and Scedrov.
Even though they have captured the notion of subtype as being related to
coercions (from the subtype to the supertype), it is not yet clear to me
how that style of model could capture notions like record update (I realize
that bounded fun cannot express this notion, I am concerned about what
a model would look like for a new and improved version of the language which
did allow such expressions).
Let me explain. The more I look at object-oriented programming, the
more I believe that there are at least two different, perhaps equally important,
notions floating around. One certainly is the notion of inheritance of
representation of subtype from a supertype (this is the motivation for using
coercions to model subtype). However, equally important is the notion of
code reuse (see Liskov's article in the supplement to OOPSLA '87, among others,
for some hints on this). That is, because of structural considerations, if I
have a function which does things to certain fields of a record, then it will
also work similarly on another record type that has (at least) those same
fields. In most object-oriented languages, these two uses seem to be mushed
together, although this does not seem necessary.
The general model definition given in Bruce-Longo tried to capture
both of these notions (although it may have intertwined them more than
necessary), as did the particular model built from PER's. If we could
reformulate that particular model to eliminate the problem of "too many
subtypes," I think that it would be quite good for both of those purposes,
hopefully even with a new more expressive language.
It is clear how the Breazu-Tannen, Gunter, and Scedrov model handles
the first of these notions (inheritance of representation), but it is not
clear to me how it would handle code reuse. How would that model handle
functions which only make sense when applied to record types with at least
fields I, J, K, each of type integer? I'm not saying that it can't, just
that I don't see how it does, based on the information that has come across the
types list so far. Perhaps my problem is based on a simple misunderstanding
of their model, or can be solved in some simple way. I look forward to
more progress on these issues.
Kim Bruce