A type * S* is a

`T`

`S`

`T`

`S`

`T`

A type * U* is a

`T`

`T`

`U`

Subtyping is reflexive: * S* ≤

`S`

`S`

`T`

`T`

`U`

`S`

`U`

If an expression has type * S*, and

`S`

`T`

`T`

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`

`U`

`S`

`U`

`T`

`U`

`S`

`T`

`S`

`T`

`S`

`T`

Some common cases:

The join of

and`T`

is`T`

.`T`

If

≤`S`

, then the join of`T`

and`S`

is`T`

.`T`

The join of

and`T`

`Top`

is`Top`

.The join of

and`T`

`Bot`

is.`T`

The join of two unrelated types is usually `Top`

.

A *common subtype* of two types * S* and

`T`

`U`

`U`

`S`

`U`

`T`

`S`

`T`

`S`

`T`

`S`

`T`

Some common cases:

The meet of

and`T`

is`T`

.`T`

If

≤`S`

, then the meet of`T`

and`S`

is`T`

.`S`

The meet of

and`T`

`Top`

is.`T`

The meet of

and`T`

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

`T`

`C`

`C`

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**