This is a demonstration that we may view traits as type constructors: that is, functions from Type to Type. This view is motivated from a categorical perspective of type theory, in which the morphisms of the category take the central role. Cf. subobjects, which are represented by morphisms, rather than objects in a different category.
I'm assuming that the category of types, Type, is bicartesian closed. The set of morphisms between
any two objects includes the set of functions denoted by Fn, FnMut and FnOnce in Rust.
Given a trait with associated types X_0, X_1, ..., X_m and associated function types F_0, F_1, ..., F_n, we define the trait function as a function T from Type -> Type taking each object A to the object T(A) := A + A × ((i: Fin(m)) -> Type) × ∏ (j: Fin(n)) F_j, where Fin(k) is the set of natural numbers less than k.
Note that for all types A: Ob(Type), we have an embedding A -> T(A) given by ι_1 (the first injection).
Given a type A, and an implementation of T for A, defining types X_i := Y_i for all i ∈ Fin(m) and functions f_j: F_j for all j ∈ Fin(n), we have a morphism A -> T(A) given by λ (a: A). ι_2 (a, λ (i: Fin(m)). Y_i, λ (j: Fn(n)). f_j), known as the implementation morphism.
In order to construct a type conditional on some trait bound requiring a type A to implement the aforementioned trait, it suffices to depend on a function B with the type A -> A × ((i: Fin(m)) -> Type) × ∏ (j: Fin(n)) F_j, known as a bounding function. The codomain of B gives the implementation objects of T for B.
Note that we have already given constructions of bounding functions for all implementations of traits. Given a bounding function, we may always construct a morphism to
Now, we may define the relationship of these four concepts to the language features in Rust.
- A trait is represented by a trait function.
- An implementation of a trait is given by an implementation morphism.
- A trait bound is given by a bounding function.
- Casting a type to a trait (the
<A as T>syntax) is given by an implementation object.
Furthermore, given a canonical set of implementation morphisms (corresponding to the set of impls
in a single Rust program), the trait function T has the structure of a functor, whose map on
morphisms takes a function f: A -> B to the function T(f) given by r_B ∘ f ∘ π_1, where π_1 is the
first projection and r_B is the implementation morphism for T for B. There are a number of nice
corollaries, such as the implementation morphisms forming a natural transformation from Id => T and
each pair (A, r_A) having the structure of a T-coalgebra.