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

RE: Subject reduction fails in Java - Part 2

Can this be summarized by saying that a language ought to provide type
abstraction mechanisms that allow you to reveal only that a type t is a
subtype of another type T in a given context?  The presence of such a
construct is completely compatible with structural subtyping; it's just that
in some contexts we hold a type t (partially) abstract by revealing only
that t <: T.  In other words: one shouldn't decide as a language design
issue that types compare structurally or not, but rather whether the
language should support constructs to restrict knowledge about subtyping
relationships in certain contexts.

Bob Harper

-----Original Message-----
From: Gary T. Leavens [mailto:leavens@cs.iastate.edu]
Sent: Saturday, June 20, 1998 2:07 PM
To: kim@bull.cs.williams.edu
Cc: types@cs.indiana.edu; leavens@cs.iastate.edu
Subject: Re: Subject reduction fails in Java - Part 2


[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

Kim Bruce writes:

> I'd be interested in hearing if anyone feels there are strong advantages
> to "by declaration" subtyping versus structural subtyping.

One possible advantage of "by declaration" (or "by name" or
"occurrence") subtyping is that the programmer can inform the type
system of behavioral subtype relationships.  Most type systems do not
express information about behavioral specifications, and most
langauge implementations, even if they had such information, would not
want to do the theorem proving required to prove behavioral subtyping
relationships structurally, as that is undecideable in general.
(An exception is Abadi and Leino's work [1].)  Furthermore,
it is useful to have the type system check that only behavioral subtypes
are used as subtypes, as that automates part of the verification of OO
programs.

Moreover, when a language has a declaration that says that a type is
a subtype of some other type(s), one can automatically introduce proof
obligations for the subtype, or use specification inheritance to force
behavioral subtype relationships (as in [2]).  If potential supertypes
are unknown, then a verification logic has no way to do introduce these
proof obligations once and for all, but instead must introduce them at
each point of use of one type as a subtype of another (as described
above).

That said, as a Java programmer, I've often wished for structural
subtyping, as it's impossible to provide, for example, a reusable
container class that relies on the elements implementing some
interface.  You simply can't expect that other people would know enough
to implement that interface ahead of time.
I expect that the same arguments also apply to behavioral subtyping, so
it may be, in the end, that we want to make verification logics (like
[1]) that do this structurally as well, trading complications in the
logic for more reuse.


REFERENCES

[1] Martin Abadi and Rustan Leino.  A Logic of Object-Oriented Programs.
    In Michel Bidoit and Max Dauchet (eds.), TAPSOFT '97: Theory and
    Practice of Software Development, 7th International Joint Conference
    CAAP/FASE, Lille, France, pages 682-696.  Volume 1214 of Lecture Notes
in
    Computer Science, Springer-Verlag 1997.

[2] Krishna Kishore Dhara and Gary T. Leavens.
    Forcing Behavioral Subtyping Through Specification Inheritance.
    In Proceedings 18th International Conference on
    Software Engineering, Berlin, Germany, pages 258-267. IEEE, 1996.
    An extended and slightly revised version is
    Department of Computer Science, Iowa State University,
    TR #95-20c, March 1997.
    ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz

	Gary