Nov 10, 2026

Formalizing Rust: Subtyping and Variance

In Rust, we often implicitly use subtyping and variance to analyze how lifetime relationships change inside nested types. This article is my attempt to formalize those concepts! It is a work in progress and will be updated as I learn more about programming language theory.

My goal is to write more articles on the formalization of Rust to connect everything together, but for now, those of you here will need an understanding of lifetimes, traits, and smart pointers.

Subtyping

Definition (Subtyping).

$T$ is a subtype of $U$ , denoted $T\le U$ , if a value of type $T$ can be treated as a value of type $U$ without requiring coercion.

This is usually seen in the context of lifetimes. If the lifetime 'a outlives 'b (written in code as 'a: 'b), then &'a T is a subtype of &'b T. Intuitively, this should make sense: a longer lifetime can take the place of a parameter that requires a shorter lifetime without any problems. But to describe it formally, we would need to show that &'a T is covariant over 'a — more on that later!

Note that trait bounds do not establish subtyping relationships. One example is how Copy is a subtrait of Clone, i.e., Copy: Clone. This means that every type implementing Copy must also implement Clone, but it does not establish any subtyping relationships between concrete types. Instead, trait bounds simply restrict which types may be used as generic parameters.

This should not be confused with trait objects, which can involve subtyping relationships between lifetime bounds! For any trait R, dyn R + 'a is a subtype of dyn R + 'b if 'a outlives 'b. This also applies to trait objects with higher-ranked lifetime bounds like dyn for<'a> R<'a>, which can be subtypes of corresponding trait objects with lifetimes substituted for 'a. However, trait objects do not have subtyping relationships between different traits. For example, if S: R, then dyn S can be coerced to dyn R through trait upcasting, but dyn S is not a subtype of dyn R.

Theorem (Subtyping is a Partial Order).

The subtyping relation $\le$ is a partial order up to type equivalence, meaning it satisfies the following properties.

Reflexivity: For any type $T$ , $T \le T$ .
Antisymmetry: For all types $T, U$ , if $T \le U$ and $U \le T$ , then $T = U$ .
Transitivity: For all types $T, U, V$ , if $T \le U$ and $U \le V$ , then $T \le V$ .

Variance

Definition (Type Constructor).

A type constructor is a parameterized type that produces a type when its parameters are specified. For example, Vec<T> is a type constructor that produces types such as Vec<i32> and Vec<String>.

Definition (Covariance).

A type constructor $F$ is covariant over a parameter $T$ if for any parameter $U$ ,

T \le U \implies F(T) \le F(U)

Theorem (Covariance of Immutable References).

$\& \text{'a } T$ is covariant over $\text{'a}$ and $T$ .

Theorem (Covariance of Mutable References Over Lifetimes).

$\& \text{'a mut } T$ is covariant over $\text{'a}$ .

Theorem (Covariance of Owned Types).

Owned types generic over $T$ are covariant over $T$ .

Theorem (Covariance of Function Outputs).

$T \rightarrow U$ is covariant over $U$ .

Definition (Contravariance).

A type constructor $F$ is contravariant over a parameter $T$ if for any parameter $U$ ,

T \le U \implies F(U) \le F(T)

Theorem (Contravariance of Function Inputs).

$T \rightarrow U$ is contravariant over $T$ .

Definition (Variance).

A type constructor $F$ is variant over a parameter $T$ if $F$ is either covariant or contravariant.

Definition (Invariance).

A type constructor $F$ is invariant over a parameter $T$ if $F$ is neither covariant nor contravariant.

Theorem (Invariance of Mutable References Over Types).

$\& \text{'a mut } T$ is invariant over $T$ .

Theorem (Invariance of Interior Mutability Types).

Interior mutability types generic over $T$ are invariant over $T$ .