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: T := E
is legal in the presence of subtyping. Once the assignment has occurred,
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:
-
- 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 subtype relation is defined in terms of a checklist of properties that must hold between the specifications of the two types,
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):
- 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).
- Subtype constraints ensure supertype constraints. S’s type constraint implies T’s type constraint (under the abstraction function).
Why does this subtype relation guarantee that the No Surprises Requirement holds? Recall that the Requirement refers vaguely to "properties." What this definition of subtype guarantees is that certain properties of the supertype - those that are stated explicitly or provable from a type's specification - are preserved by the subtype.
" (end of extract)
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
Wing On Types