Type Constructor

type-theory

Definition

Type Constructor

Let $\mathcal{T}$ be the set of all concrete types, i.e. the universe of types. A type constructor $K$ is a mapping (function) from the universe of types to itself:

$$K:\mathcal{T}\to \mathcal{T}$$

Let $K[A]$ denote the application of the type $A$ to the constructor $K$ to produce a new concrete type.

Variance

Covariant

Definition

Covariant Type Constructor

Let $A$ and $B$ be type. A type constructor $K$ is called covariant if it preserves the subtype relation of the types:

$$A\le B⟹K[A]\le K[B]$$

where $(\cdot \le \cdot )$ denotes the subtype relation.

Link to original

Contravariant

Definition

Contravariant Type Constructor

Let $A$ and $B$ be type. A type constructor $K$ is called contravariant if it reverses the subtype relation of the types:

$$A\le B⟹K[B]\le K[A]$$

where $(\cdot \le \cdot )$ denotes the subtype relation.

Link to original

Invariant

Definition

Invariant Type Constructor

Let $A$ and $B$ be type. A type constructor $K$ is called invariant if it is neither covariant nor contravariant:

$$A\le B⟹\left(K[A]\cancel{\le }K[B]\wedge K[B]\cancel{\le }K[A]\right)$$

where $(\cdot \le \cdot )$ denotes the subtype relation.

Link to original