From JeannetteWing?'s extended abstract on http://reports-archive.adm.cs.cmu.edu/anon/1997/abstracts/97-121.html. Summarizing one snapshot of current research in TypeTheory.

(start of extract) " The programming language community has come up with many definitions of the subtype relation. The goal is to determine when this assignment*x* will be used according to its `apparent' type *T*, with the expectation that if the program performs correctly when the actual type of *x*'s object is *T*, it will also work correctly if the actual type of the object denoted by *x* is a subtype of *T*.
... Moreover, unexpected behavior that can result from one user changing an object with respect to another user's viewpoint is more likely since users may be unaware of each other's existence.
Programmers make two kinds of changes to a supertype definition when defining a subtype: they add new methods and they change old methods of the supertype. Unconstrained, however, both kinds of modifications can can lead to surprising behavior. Consider a type fat_set that has only *create*, *insert*, and *size* methods. If we were to define a subtype, set, by adding a new method, *delete*, then suddenly the fact that a fat_set object can only grow in size no longer is true, surprising users who think they have a fat_set object when it really is a set object. So, we cannot just add methods willy-nilly. *...*
What we need is a subtype requirement that constrains the behavior of subtypes so that users will not encounter any surprises:
*S* and *T*. Since in general the value space for objects of type *S* will be different from the
value space for those of type *T* we need to relate the different value spaces; we use an *abstraction function*, *A*, to define this relationship. Also since in general the names of the methods of type *S* can be different from those of type *T* we need to relate which method of *S* corresponds to which method of *T*; we use a *renaming* map, *R*, to define this correspondence. (In a programming language like Java, this is just the identity map, as realized though method overloading.)
*S* is a *subtype* of *T* if the following three conditions hold (informally stated):

This seems eminently sensible. What I mean by that, of course, is that it's exactly what I've always thought! -- TomAnderson*This is simply the application of the PrincipleOfLeastAstonishment to this particular problem.*

CategoryLanguageTyping

(start of extract) " The programming language community has come up with many definitions of the subtype relation. The goal is to determine when this assignment

*x: T := E*

*No Surprises Requirement*: Properties that users rely on to hold of an object of a type*T*should hold even if the object is actually a member of a subtype*S*of*T*.

- The abstraction function respects the invariants. If the subtype invariant holds for any subtype value,
*s*, then the supertype invariant must hold for the abstracted supertype value*A*(*s*). - Subtype methods preserve the supertype methods' behavior. If
*m*is a subtype method then let*n*be the corresponding*R*(*m*) method of the supertype.- Arguments to
*m*are contravariant to the corresponding arguments to*n*;*m*'s result is covariant to the result of*n*. - Any exception signaled by
*m*is contained in the set of exceptions signaled by*n*. -
*n*’s pre-condition implies*m*’s and*m*’s post-condition implies*n*’s (under the abstraction function).

- Arguments to
- Subtype constraints ensure supertype constraints.
*S*’s type constraint implies*T*’s type constraint (under the abstraction function).

This seems eminently sensible. What I mean by that, of course, is that it's exactly what I've always thought! -- TomAnderson

CategoryLanguageTyping

View edit of May 14, 2004 or FindPage with title or text search