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 impl
s
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.