Understanding Subtyping in Rust

Author: Justin Restivo
Date: 2022-06-25

1 Expected background

This post to targets folks with Rust experience.

2 Background: Categories and Functors

Contravariance and covariance are best understood with a healthy dose of category theory.

2.1 Categories

The first step is to understand a category. Hand-waving formalism, a category can be understood as:

A set of objects.
A set of arrows between objects, called morphisms. For a morphism from object to object we define a morphism as .

At this point, this should feel very similar to a DAG. We also want to be able to traverse with morphisms. This introduces a binary operator, , to compose morphisms such that morphisms in a way that allows for both identity and associativity. The identity law states that every object has an arrow pointing to itself. We call this 's identity morphism and denote it . Associativity means that morphisms associate together.

More formally (using for composition), and assuming:

are objects in a category, C

Our laws on composition become:

if exist, then the morphisms and exist and are the same morphism.
For every object in , there exists an identity morphism id_x id_x defined as such that composing this identity morphism with any morphism either into or out of is that morphism. That is, for some object if morphism exists then is . And, for some object , if morphism exists, then is .

2.2 Functors

At a high level, a functor is a mapping between two categories. Denote these categories . Then we have two surjective mappings: one from objects in category to objects in category , and another mapping for morphisms in category to morphisms in category . Note that surjective here means all objects and morphisms in are mapped.

2.3 Covariant functors

With covariant functors, the morphism mappings must preserve identity and composition. Suppose we have two objects and in category that we map to objects and in category . The identity preservation is done by forcing the morphism in category to map to in category .

The composition property means that composition of morphisms done in category must be preserved in category . E.g. if I start on object , go through object to object all in category , then I should be able to follow the mapped morphisms to go from through to in category .

Covariant functors preserve the direction of morphisms. Then suppose in category we have a morphism . This means the morphism in category will be due to the composition preservation (compose with identity on either or ).

2.4 Contravariant functors

Contravariant functors are also a mapping, but they flip the requirements: identity is preserved but composition is reversed in the target category. So is mapped to .

2.5 Product category

A product category is defined to be a sort of "product" of categories and . Specifically, an object in is defined for every two objects in and . So, if is defined in and is defined in , then must be an object in . Morphisms in only exist if their respective morphisms exist in and .

2.6 Bifunctors

Bifunctors are functors defined over a product category.

3 Subtyping

Across programming languages, one may encounter a subtyping operator <: <: . This binary operator when used on two "things" a, b a, b as a <: b a <: b means a a is a subtype of b b . More intuitively, 'a <: 'b 'a <: 'b means 'a 'a can be used everywhere 'b 'b is used. The examples in the rust docs give the example of animals. A dog is an animal because one may use a dog wherever one uses an animal.

What does "things" mean? That is, what are a a and b b ? Typically in programming languages, subtyping is defined on the programming language's base kind. In Haskell, this is Type Type . But, Rust has two base kinds: Type Type and Lifetime Lifetime . So, Rust may have Type Type s subtyping other Type Type s, and lifetimes subtyping other lifetimes.

3.1 Rust Subtyping

With Rust types, the intuition (as made in the rustnomicon) is that of the Cat Cat and Dog Dog example. If type Cat Cat subtypes type Animal Animal , then Animal Animal is more general than Cat Cat , and we may use Cat Cat wherever we use Animal Animal since Cat Cat is an animal. But, in Rust, there is no Cat Cat or Dog Dog . Instead, Rust only does subtyping on the same type constructor (though this may be generic).

Rust lifetimes have a similar idea to the Cat Cat and Animal Animal example. If 'long <: 'short 'long <: 'short (where 'long 'long and 'short 'short are lifetimes), then we may use the variable with lifetime 'long 'long everywhere 'short 'short may be used. The intuition is since 'a 'a lives longer than 'b 'b , then we may use variables that live 'a 'a long everywhere variables with 'b 'b are used without worrying about them being freed.

A graphic diagram should explain this intuition:

'long 'short | time (increasing)
 |           |
 -------->   | start 'long
 |           |
 |           |
 |           |
 |     -->   | start 'short
 |     |     |
 |     |     |
 |     |     |
 |     -->   | end 'short
 |           |
 |           |
 |           |
 |           |
 |           |
 -------->   | end 'long
             |

'long 'short | time (increasing)
 |           |
 -------->   | start 'long
 |           |
 |           |
 |           |
 |     -->   | start 'short
 |     |     |
 |     |     |
 |     |     |
 |     -->   | end 'short
 |           |
 |           |
 |           |
 |           |
 |           |
 -------->   | end 'long
             |

Practically, 'static 'static subtypes every lifetime since it is defined to be the longest living lifetime (it lives for the entire program).

3.2 Rust Subtyping Inference

Rust's subtyping inference rules begin with lifetimes. Rust infers the lifetime length and then lifetime subtyping relations. Then, Rust infers subtyping relations on Types.

The second way Rust is able to subtype is by using several specific rules over types based on their input lifetime parameters. For example, if 'static <: 'a 'static <: 'a , then &'static str <: &'a str &'static str <: &'a str . Note this is just an example, and we haven't discussed why this is true. Now, consider the following chart:

4 Covariant example

Let's build up intuition for these inference rules via a few examples, starting with &'a T &'a T . & & is a type constructor that takes in two arguments: a lifetime and a type. This may be thought of as a bifunctor. The category the bifunctor maps from is a product category. The two categories used to create this product category are essentially:

Then, the product category we're mapping from is then , and the category we map to is . The implication is: 'a <: ' b, T <: U 'a <: ' b, T <: U &'a T <: &'b U &'a T <: &'b U exactly because ('a, T) ('a, T) and ('b, U) ('b, U) are objects in the input category . Since and in the indiviual categories, ('a, T) ('a, T) ('b, U) ('b, U) must be a morphism in the product category by definition. And this maps to & 'a T & 'a T &'b U &'b U in the output . The map is a subtyping relationship.

Intuitively, this should also make sense: &'a T &'a T can be used everywhere &'b U &'b U is used for two reasons. First, T T can be used everywhere U U is used. Secondly, 'a 'a (which is the lifetime of & & ) lives longer than 'b 'b so there are no worries about use after free.

5 Contravariant Example

There are other covariant examples with functors (and bifunctors) that work very similarly to the prior example. There is, however, one contravariant example: function types. In this case, we have that: S <: T, U <: V => fn(T) -> U <: fn(S) -> V S <: T, U <: V => fn(T) -> U <: fn(S) -> V

This construction should make sense from a category point of view. The input category is the product category and the bifunctor maps to . The difference here is the usage of the opposite cateogry. This category takes the input category and flips the direction of all its morphisms. This essentially means that the mapping is contravariant in the first argument. So for objects , morphisms only exist in the output category when morphisms (notice this is flipped!) and exist in the input to the product category.

For simplicity, denote:

Then f <: g f <: g .

I'm simplifying this but, the intuition for this subtyping relation can be thought of as enforcing lifetimes. If we want to be able to use f f everywhere that we can use g g , then the arguments to f f cannot be used as long as long as the arguments to g g . And the returned type must live longer than that of g g so we can use it as we might use g g 's output. All this is doing is enforcing that with lifetimes.

6 Invariant

Invariant in this case simply means with any sort of functor we define (covariant or contravariant), there is no morphism mapping that makes sense. These are like Cat Cat and Dog Dog – a subtyping relationship does not make sense.

7 Struct Type Example

Let's also consider a simplified example from the rust reference

use std::cell::UnsafeCell;
struct Variance<'a, T, U: 'a> {
    x: &'a U,               // This makes `Variance` covariant in 'a, and would
                            // make it covariant in U, but U is used later
    y: *const T,            // Covariant in T
}

use std::cell::UnsafeCell;
struct Variance<'a, T, U: 'a> {
    x: &'a U,               // This makes `Variance` covariant in 'a, and would
                            // make it covariant in U, but U is used later
    y: *const T,            // Covariant in T
}

This is defining a product category: . The subtyping rules from above apply to the innards of the struct and therefore the struct itself. We simply have morphisms on the output category when both functors map.