## 9.3. Subtyping

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`.

### 9.3.1. Top

`Top` is the universal type. Every value has type `Top`. Every type is a subtype of `Top`.

### 9.3.2. 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.

### 9.3.3. Join

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`.

### 9.3.4. Meet

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`.

### 9.3.5. Variance

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:

• `C` is covariant if `S``T` implies that `C`{`S`} ≤ `C`{`T`}

• `C` is contravariant if `S``T` implies that `C`{`T`} ≤ `C`{`S`}

• `C` is invariant if `S` = `T` implies that `C`{`S`} = `C`{`T`}.

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.