 | ||
|---|---|---|
 | Chapter 9. Type System |  |
| 9.2. Parametric Polymorphism | 9.3. Subtyping | 9.4. Adding Type Information |
A type S is a subtype of a type T, written S ≤ T,
if a value of type S can be used in any context expecting a value of type T.
A type U is a supertype of a type T if T ≤ U.
Subtyping is reflexive: S ≤ S. Subtyping is also
transitive: if S ≤ T and T ≤ U,
then S ≤ U.
If an expression has type S, and S ≤ T,
then that expression also has type T. This is called subsumption.
Types in Orc form a bounded lattice. The lattice is ordered by the subtyping relation,
its maximal element is the special type Top, and its minimal element is
the special type Bot.
Bot is the empty type.
No value has type Bot.
Bot is a subtype of every type.
An expression has type Bot only if it is silent.
Bot has an interesting status in Orc. In other typed languages, if an expression
has type Bot, this usually indicates a guaranteed error, infinite loop, or other failure
to return a value. Since sequential programming rarely involves subexpressions that are guaranteed
never to return, Bot is usually just a curiosity or a formal artifact of the type system,
and indeed many type systems do not have a Bot type at all.
In Orc, however, Bot is very useful, since it is frequently the case that Orc expressions
are written to carry out ongoing concurrent activities but never publish any values, and the type system
can use the type Bot to indicate that no publications will ever be seen from such
expressions.
A common supertype of two types S and T is any type U such that
S ≤ U and T ≤ U.
The join of S and T is the least common
supertype of S and T: it is a subtype of every common supertype of S and T.
Some common cases:
The join of T and T is T.
If S ≤ T, then the join of S and T is T.
The join of T and Top is Top.
The join of T and Bot is T.
The join of two unrelated types is usually Top.
A common subtype of two types S and T is any type U such that
U ≤ S and U ≤ T.
The meet of S and T is the greatest common
subtype of S and T: it is a supertype of every common subtype of S and T.
Some common cases:
The meet of T and T is T.
If S ≤ T, then the meet of S and T is S.
The meet of T and Top is T.
The meet of T and Bot is Bot.
The meet of two unrelated types is usually Bot.
When types contain other types as components, such as a tuple type or a polymorphic type, the
subtype relationship between these composite types depends on the subtype relationships between
their components. Suppose we have a composite type of the form C{T},
where T is a type and C is the context in
which it appears. The variance
of the context C is defined in the standard way:
Tuple types, record types, and list types are all covariant contexts. In a function type, the return type is a covariant context, but the argument types are contravariant contexts. The type parameters of mutable object types are invariant contexts.
The variance of the type parameters in an aliased type or datatype is determined from the declaration itself, by observing the contexts in which the parameters appear. If a parameter appears only in covariant contexts, it is covariant. If it appears only in contravariant contexts, it is contravariant. If it appears in both contexts, it is invariant.
Related Reference Topics