Types and subtypes

  A type in a programming language represents a set of values and the operations and relations that are applicable to them. For example the ${\it {Integer}}$ type represents the set of whole numbers and the usual integer operations and relations, including =, <, >, +, -, *, div, and mod.

Strongly typed languages provide type-checking mechanisms to ensure that nonsensical operations are not applied to values. Such a language is sometimes said to be type safe . For example a strongly typed language will ensure that two characters are not added together as though they were integers. While these type checks can be provided at run-time, in this paper we will concentrate on static or compile-time type-checking mechanisms.

In statically-typed programming languages like Pascal and C, expressions as well as values are given types. A static type checking system determines in which contexts an expression may legitimately occur. A correct static type checker should guarantee that the value of a type-checked expression is compatible with its static type. Thus if the variable ${\it {x}}$ is declared to have type ${\it {Integer}}$, a static type system will assign the expression ${\it {x + 1}}$ the type ${\it {Integer}}$, which guarantees that the value of the expression at run-time will be an integer.

In object-oriented languages, the most important operation is sending a message to an object. In this case one goal of type checking is to ensure that inappropriate messages are not sent to objects. In particular if a message is sent to an object, the type system should ensure that the object has a method with the same name, and that the formal parameter and return types are compatible with those of the call. From a typing point of view, then, a message send to an object is similar to extracting a field from a record in which the field happens to be a function.

The reader is refered to [CW85] for a more extensive discussion of the role of types in programming languages.

A type ${\it {S}}$ is a subtype of a type ${\it {T}}$ (written ${\it {S {\rm \ <: \ }T}}$) if an expression of type ${\it {S}}$ can be used in any context that expects an element of type ${\it {T}}$. Another way of putting this is that any expression of type ${\it {S}}$ can masquerade as an expression of type ${\it {T}}$. This definition is usually expressed in typing rules by adding a subsumption rule stating that if ${\it {S {\rm \ <: \ }T}}$ and expression ${\it {e}}$ has type ${\it {S}}$ then ${\it {e}}$ also has type ${\it {T}}$. (As we shall see later, subtyping can also be exploited in constraining polymorphic definitions.) Thus in a type system with subsumption, if an expression can be assigned a type ${\it {T}}$, it can also be assigned any type that is a supertype of ${\it {T}}$. This is in contrast to languages without subtyping in which most expressions can be assigned a unique type.

The support for subtyping provides added flexibility in constructing legal expressions of a language. For instance, let ${\it {x}}$ be a variable of type ${\it {T}}$. If ${\it {e}}$ is an expression of type ${\it {T}}$, then ${\it {x := e}}$ is a legal assignment statement. If ${\it {S}}$ is a subtype of ${\it {T}}$ and ${\it {e'}}$ has type ${\it {S}}$, then ${\it {x := e'}}$ will also be a legal assignment statement by the subsumption rule. Similarly an actual parameter of type ${\it {S}}$ may be used in a function or procedure call when the corresponding formal parameter's type is declared to be ${\it {T}}$. In most pure object-oriented languages, these mechanisms are supported by holding objects as implicit references, interpreting assignment as sharing, and passing parameters by sharing (like CLU).

How can we determine when one type is a subtype of another? A technical discussion of this topic would take us far afield from the aims of this paper into the realm of programming language semantics and type theory. Instead we will present intuitive arguments for determining when two types are subtypes. Rest assured that the intuition can be backed up by more formal semantic arguments. Because the typing of message sends has similarities to typing records of functions, we begin with examining the simpler cases of record and function types now, holding off on object types until later. We also include a discussion of references (i.e., types of variables) here, in order to prepare for the later discussion of instance variables in objects. The subtyping rules in the rest of this section are based on those given by Cardelli [Car88a].