Replacing subtyping with matching

 

You know you have achieved perfection of design, not when you have nothing more to add, but when you have nothing more to take away. Antoine de Saint Exupery

At this point we have an extremely flexible static typing system for object-oriented languages. Method types may be replaced by subtypes in subclasses, MyType supports automatic updating of parameter types in important special cases, while a combination of MyType and bounded matching provides support for safe uses of covariance in parameter types. While contravariant occurrences of MyType do cause a loss of subtyping, the matching relation (which is preserved by subclasses) appears to be more important in type checking message sends and in restricting polymorphic types. Most important of all, we have a type system that is provably type safe (see [BSvG95] for formal details of a type system, an operational semantics, and a proof of type safety for a language similar to what has been described here).

Not surprisingly, this has come at some increased cost in complexity. While a strong case can be made that any language (object-oriented or not) should support some version of bounded polymorphism, the bounds must be specified using the new relation, matching, rather than subtyping. More troubling, the difference between subtyping and matching on object types is very subtle, depending only on the absence of contravariant occurrences of MyType.

When faced with such a system, it is reasonable to look for ways to reduce complexity. The existence of two relations as similar as subtyping and matching raises the question of whether both are really necessary. We were forced to introduce matching as a way of capturing the relation between types of objects generated by superclasses and subclasses. This notion proved to be important in type checking method bodies and in defining the set of types to which a parameterized type or class could be applied. A case can be made that matching is more natural than subtyping for object types because it is simpler (no need to worry about contravariant occurrences of MyType). An argument could also be made that most object-oriented programmers would, in fact, give the definition of matching if asked to define subtyping for object types in such a system.

In the rest of this section we introduce a new experimental typing system for object-oriented languages that drops subtyping entirely in favor of matching. To accomplish this we introduce one new construct involving matching in order to recapture some of the flexibility of subtyping.

In section 4 we eased the restrictions on changing types of methods in subclasses to replace the types of methods by subtypes. While this provided us with a somewhat more flexible type system, it is interesting to note that none of the examples examined once we introduced MyType actually took advantage of this flexibility. The use of MyType took care of most of the desired flexibility, and the other examples where covariance in parameters or instance variables seemed to be needed were not helped by allowing subtyping of method types. Instead, they required the introduction of bounded matching to attain the flexibility needed. Thus, it is reasonable to wonder whether it was really necessary to allow methods in subclasses to have types that are subtypes of those in the superclass.

As expected, the notion of matching will play a key role in replacing subtyping. In section 5, matching was defined in terms of subtyping of corresponding method types. Since we now wish matching to be primitive, we give a new more restrictive definition of matching. We define

$${\rm{\it {ObjectType\{m_i:T_i\}}}}_{1 \le i\le k} {\rm \, <\... ...{O}}}bjectType\{m_i:T_i\}}_{1 \le i \le n}\mbox{ iff } n \le k.$$

Thus one object type matches another if the first can be obtained by adding more methods to the second. No method types may be changed in object types that match. (Of course, as before, occurrences of MyType mark places where types automatically change meaning.)

All previous uses of subtyping in parameters that are of object type could be replaced by polymorphic functions using bounded matching. Thus a function ${\it {f}}$ to be used with objects of any type that matches type ${\it {Window}}$ could be written:

$${{\rm{\it {function\ f(W {\rm \, <\!\!\!\char93 \, }Window,\ w:\ W)\ ...}}}}$$

Unfortunately, this notation is a bit heavy, and programmers are not likely to enjoy passing around type parameters everywhere that they formerly used subtyping.

To remedy this we introduce a new type constructor. If ${\it {T}}$ is an object type, then #T will also be a type. An element will have type #T if it has any type that matches ${\it {T}}$. That is, if ${\it {a}}$ has type ${\it {S}}$ and ${\it {S {\rm \, <\!\!\!\char93 \, }T}}$then ${\it {a}}$ also has type #T. We also have a form of subsumption with #-types. If ${\it {S {\rm \, <\!\!\!\char93 \, }T}}$ and ${\it {a}}$ has type #S then ${\it {a}}$ also has type #T. (A similar kind of notation occurs in [Car88b], where power types are introduced to stand for the collection of types which are subtypes of a given type. Ada 95 [Int95] also includes a similar notation, written ${\it {T'Class}}$, to designate the collection of types which are subclasses of ${\it {T}}$.)

We can now rewrite the declaration of the function ${\it {f}}$ above as follows:

$${{\rm{\it {function\ f(w:\ {\rm\char93 {\it {Window}}})\ ...}}}}$$

Thus ${\it {f}}$ can be applied to any value with a type that matches ${\it {Window}}$. Note that this offers at least the flexibility of subtyping. In fact, if ${\it {Window}}$ contains any binary methods, it will have no non-trivial subtypes, while there are many types that would match it. While only object types can be annotated with # in order to get the effect of subtyping, in most object-oriented languages, only object types and simple types are available to be passed as parameters. (If the language does not interpret record types as degenerate object types, one could define a notion of matching for record types in which matching is simply record extension.)

We have emulated subtyping of function parameters with #-types, but what about the other important use of subtyping, making assignments to variables? This case is more difficult in that this use cannot be easily expressed with bounded matching. However, we can take our #-types seriously, and use them to provide types for variables that are intended to hold values of multiple types. If ${\it {x:\ {\rm\char93 {\it {T}}}}}$ is a variable declaration and ${\it {e:\ S}}$ for ${\it {S {\rm \, <\!\!\!\char93 \, }T}}$, then ${\it {x}}$ := ${\it {e}}$ will be type-correct.

We emphasize that this is no longer an abbreviation for a use of bounded matching. It is an entirely new type construct. The introduction of #-types makes it easier for a programmer to express more precisely his/her intentions.

For example, suppose that we define the type function ${\it { List}}$ as in Figure 14. In a language with subtyping, if we applied ${\it { List}}$ to a type ${\it {S}}$, the list could also hold elements of any subtype of ${\it {S}}$. Of course, if ${\it {S}}$ has binary methods, it will not have non-trivial subtypes, and we could not have a heterogeneous list of these elements. The point is that the choice of whether the list is homogeneous or heterogeneous is determined not by the programmer, but depends only on whether or not ${\it {S}}$ has a binary method.

In the language we propose here without subtyping, applying ${\it { List}}$ to type ${\it {S}}$ would provide the interface for a homogeneous list: all of the elements would have exactly type ${\it {S}}$. We can also provide a list definition using #-types that will give us a heterogeneous list. Thus a language with #-types provides the programmer with much greater expressiveness by allowing the choice of either homogeneous or heterogeneous data structures.

In Appendix A we provide an extended example of the definition of a heterogeneous list in a language with #-types. As in the example, one would normally wish to restrict the elements of heterogeneous data structures to have types which match a fixed type (in this case, the type ${\it {rect\_type}}$). This is generally necessary to determine the collection of methods that can be applied to all elements of the data structure.

This extra power and flexibility does not come entirely for free. In fact, there is one extra complication in sending messages that correspond to binary methods. If all we know about the type of an expression is that it matches a particular type, then we cannot send it a message which corresponds to a binary method. This is a necessary consequence of the need in a binary method to have a parameter with exactly the same type as the receiver. If one doesn't know the exact type of the receiver, you certainly won't know what type of value to provide as the parameter.

For example, recall that in our discussion of typing in section 6, we determined that if ${\it {o:\ S}}$ and ${\it {S {\rm \, <\!\!\!\char93 \, } ObjectType\ \{m:\ T\}}}$ then the type of ${\it {o.m}}$ would be ${\it {T[S/{\rm{\it MyType}}]}}$. It was important for that rule that we knew the exact type of ${\it { o}}$ (at least up to subtype). Now what happens if ${\it { o}}$ has type #S? Since we only know ${\it { o}}$'s type up to matching, we cannot just blindly apply the usual type-checking rule. However it can be shown that if ${\it {T}}$ has no contravariant occurrences of MyType, ${\it {o.m}}$ can be given type ${\it {T[{\rm\char93 {\it {S}}}/{\rm{\it MyType}}]}}$. If ${\it {T}}$ does have contravariant occurrences of MyType (e.g., it is a binary method), then we cannot statically determine the type of ${\it {o.m}}$.

This failure to determine a type for the message send of a binary method should not be a surprise. We illustrate with the ${\it {Node}}$ example from section 6. If we only know that ${\it {n1}}$ has type #NodeType and that ${\it {n2}}$ has type ${\it {DbleNodeType}}$, then we cannot determine whether or not ${\it {n1.setPrev(n2)}}$ is legal. It will only be legal if the type of the value of ${\it {n1}}$ is exactly ${\it {DbleNodeType}}$. Any other type matching ${\it {NodeType}}$ would not result in a well-typed expression.

One practical consequence is that we can generally only send non-binary messages to elements of a heterogeneous data structure (i.e., one whose value fields are #-types) unless the language provides a type-case or other similar statement to help discriminate the types at run-time. Note however that the existence of binary methods in a type ${\it {S}}$ does not prevent the sending of non-binary messages to objects of type #S.

While forbidding binary messages to be sent to #-types might seem to be a major handicap, we have found that it proves not to be in practice. The first reason is that one rarely wants binary methods when dealing with heterogeneous data structures. In the heterogeneous list example in Appendix A, for example, the ${\it {gt}}$ and ${\it {eq}}$ methods both take parameters of type #rect_type. It would not make sense for them to take parameters of type MyType or #MyType since then you might not be able to compare two elements of the list with different types, even though both match ${\it {rect\_type}}$.

A second reason for not worrying about this limitation is that if the base type had binary methods, we could not obtain heterogeneous data structures at all in the original language with subtyping. As a result we still have more flexibility in this system. We just have to be more careful with binary methods than with those with no contravariant occurrences of MyType.

Finally, in the case where binary methods are needed, programmers will need to use explicit bounded matching rather than #-types. This way the programmer can ensure that the parameters are of the same type as the receiver. While this is a little less compact than the # types, it still gives the same flavor.

A possible disadvantage of the system described above is that we do not allow the types of methods to be explicitly changed in subclasses. (As before, they implicitly change because of occurrences of MyType.) While we believe that the constructs included in this language do provide sufficient functionality for most purposes, it is possible to generalize the definition of matching in order to support the change of methods in subclasses. In order to do this it is necessary to define a matching relation on function types, since the types of methods are functions.

This can be done in a way that provides more flexibility in defining subclasses, but we remain unconvinced that this provides enough benefit to be worth the resulting complexity. As with the examples provided earlier in this paper, most examples we have looked at can be handled easily with a combination of the simple matching presented in this section, MyType, and match-bounded polymorphism.

Another possible disadvantage of this language design is that it forces the programmer to mark those parameters and variables in a program that may later need to take values whose types only match the given types. This requirement to plan ahead is indeed a negative point in this design. However, it is worth pointing out that, despite the hype to the contrary, it already takes great care to design classes that can be successfully used to derive subclasses. This helps explain the common wisdom that good class libraries are more helpful in code reuse than libraries in traditional imperative languages, but good class libraries are much harder to design than libraries in traditional languages. Thus we would argue that good object-oriented design currently takes significant planning ahead for change on the part of the programmer. As a final justification, we note that the designers of Ada 95 made a similar decision to require the programmer to mark those variables and parameters which are allowed to hold values whose types are subtypes of a given type.

In summation, the language described in this section is considerably simpler than the language presented in the earlier sections of this paper. In spite of the elimination of subtyping from the language, the use of #-types and bounded matching seems to provide a language significantly more expressive than the object-oriented languages in common use today. In particular, the solutions to all of the problems discussed earlier in this paper are all legal programs in this new language. None of the final solutions took advantage of subtyping in any way!

Leaf Petersen and the author have designed and implemented a language, LOOM, which corresponds to the design given in this section. A technical report is currently being written which will describe the language in more detail. The paper [Pet96] presents an overview of the language and describes a module system which provides greater support for programming in the large. Our use of LOOM in working out many examples leads us to believe that it combines an appealing simplicity with sufficient expressive power to model most situations likely to arise in practice.