Rust Traits as Existential Types

Why try to model rust traits as existential types? First and foremost, it’s interesting!
But I also believe there’s satisfaction and benefit to be had in drawing connexions between related ideas and in learning the terminology used by other people.

The central idea of the essay is this:

In some sense, this essay simply shows a few program fragments being translated into different systems of notation, but the hope is actually to show how two ideas (existential types and Rust traits) are similar and how they are different. Please note that this essay is a work in progress.

We’ll present each program fragment in four systems.

• System 1 uses notation like that of type theory or programming language theory.
• System 2 is a hybrid of systems 1 and 3.
• Systems 3 and 4 use Rust syntax with some extensions.

Systems 1, 2, and 3 use λ2 or λω languages endowed with existential types, but system 4 has a separate metalanguage and language. We’ll start with λ2 and then later consider λω.

Each program fragment is presented in a box with four tabs, like so:

pair : Type = N × N
neighbors : N → Pair = λ n . ⟨ n + 7 mod 8 , n + 1 mod 8 ⟩

Pair : Type = (u64, u64)

neighbors : u64 -> Pair = lambda(n) { (n + 7 mod 8, n + 1 mod 8) }

type Pair = (u64, u64);

fn neighbors(n : u64) -> Pair
{
  return ((n + 7) % 8, (n + 1) % 8);
}

let arg_types = vec![RustType::U64];
let ret_type  = RustType::Tuple(vec![RustType::U64, RustType::U64]);

fn body(arguments : &[RustObject]) -> RustObject
{
  let [RustObject::Integer(n)] = arguments else { panic!(); };
  let prev = RustObject::Integer((n + 7) % 8);
  let next = RustObject::Integer((n + 1) % 8);
  return RustObject::Tuple(vec![prev, next]);
}

context.insert("Pair", RustItem::Type { typ: ret_type.clone() });

context.insert("neighbors", RustItem::Value {
  typ:   RustType::Function(arg_types, Box::new(ret_type)),
  value: RustObject::Function(body)
});

Since the sort of notation used in type theory or programming language theory may be unfamilar, and because we’ll depart from convention in a few places, we’ll go over the notation of system 1 before getting to existential types and traits.

If you’re familiar with the notation, however, you can jump ahead to those sections.

⊢ Notation

> The Has-Type Relation

The notation x : X means that the term x has type X. We’ll say that x is an instance or inhabitant of X. Types them­selves are inhabitants of Type, so we write X : Type. Terms which are not types we will call values (here x is an example).

We’ll generally use the name Type rather than 𝒰 (for universe), as I expect that some people may only ever read “x : T ” as “x is a T ” rather than “x has type T ” or “inhabits T ” — and the mental reading of “T : 𝒰” as “T is a universe” might be confusing, whereas reading “T : Type” as “T is a type” should be unprob­lematic. But do note that, for our purposes, the names Type and 𝒰 are equivalent.

> Brief Aside

types and sets

The way we often talk about types can encourage us to think of them as sets, but types are not collections. We can indeed consider the collection of all objects of a type — its extension — but this is distinct from the type itself (in fact, it is possible for different types to have the same extension). Whenever we say something like “the elements of a type”, this is really short­hand for “the elements of the extension of a type”. A type is defined by rules for constructing objects, and the identity (and very existence) of an object is defined by its method of construction.

There are a few short posts on the subject that might be of interest:

• Why isn’t ∈ used to denote that a value belongs to a type?
• What exactly are the semantic differences betweens sets and types?
• Types versus sets
• Type theory — Differences from set theory

> Product Types

A product type is a pair of types, and an instance of a product type is a pair of values.

⟨ x , y ⟩ : X × Y if x : X and y : Y

For convenience, we’ll actually extend this; instead of defining × to be a binary operator so that

X × Y × Z = (X × Y) × Z
⟨ ⟨ x , y ⟩ , z ⟩ : X × Y × Z

or

X × Y × Z = X × (Y × Z)
⟨ x , ⟨ y , z ⟩ ⟩ : X × Y × Z

depending on associativity, we’ll define it to be a variadic operator, so that a product type is a tuple of types.

⟨ x , y , z ⟩ : X × Y × Z

The elements of product types are usually accessed using projection functions that are defined alongside product types

t : X × Y = ⟨ x , y ⟩
π1(t) : X = x
π2(t) : Y = y

or by matching

assert (let ⟨ a , b ⟩ = t in a) = x

but we’ll also use dots for element access.

t = ⟨ x , y ⟩
t . 1 = x
t . 2 = y

> Record Types

A record type is a product type with unordered, named fields. Since the fields are unordered, it does not matter which order they are written in.

⟨ a: x , b: y , c: z ⟩ : a X × b Y × c Z

Here, a, b, and c are metavariables standing for distinct labels.

Like product types, we’ll use matching or dots for fields access.

r : a X × · · · = ⟨ a: x , . . . ⟩
r. a : X = x

Note that this use of “ : ” (for labelling the fields of a record or assigning a term to the field of a record) is entirely separate and distinct from the use of “ : ” to notate the has-type relation. Since the two meanings are unrelated (and only use the same symbol by coïncidence), the syntactic con­struc­tions are spaced differently to prevent confusion: the former only has space after the “ : ”, whereas the latter has space on both sides. I intend to write a note about this (Notating the Has-Type Relation), because the practice of writing type annotations without a space before “ : ” is a sig­nif­i­cant cause of consternation for me.

Record types with different field names are distinct, even if the constituent types are the same.

a X × c Y ≠ a X × d Y

> Function Types

These ought to be familiar.

λ x . e : S → T if x : S implies e : T
(λ x . e)  (y) = e [ y / x ]

where e [ y / x] is e with each free appearance of x replaced by y. My friend James once told me a visual mnemonic that comes to mind every time I see this notation: you can see that y replaces x (rather than the other way around) because y is hitting x over the head, driving it away.

Sometimes we might label the left-hand type with the name of the parameter.

λ x . e : x S → T

Note that functions are values, as they are instances of function types.

> Unit Type

The unit type is a type with a single inhabitant.

unit : Unit

In Rust, both the type and the value are spelled “()”, which is a 0-tuple (an empty product). In type theory, the type is sometimes named “ 1 ” and the value is sometimes named “ ⭑ ”.

The unit type is useful when a placeholder is required by the type system; for example, the return type of functions that don’t return anything explicitly is the unit type. It’s also useful in sum types, which we’ll examine next.

> Sum Types

Sum types are also known as “disjoint unions”, “discriminated unions”, or “tagged unions”.

ι 1(x) : X + Y if x : X
ι 2(y) : X + Y if y : Y

The injections “ ι 1 ” and “ ι 2 ” are usually spelled “ inl ” and “ inr ” and written without parentheses (as in “ inl x ”). [With tongue in cheek ] Presumably, the π used for projections stands for προΐημι, cognate to Latin prōiciō, whence English project is derived; then naturally, for injections, we should use ε, standing for ἐνίημι, cognate to Latin iniciō, whence English inject is derived. But ι is perhaps mnemonically more helpful, and ε is often used for empty objects.

Values of a sum type can only be used by matching:

match u with ι 1(v1) in e1 or ι 2(v2) in e2 : T
 if u : X + Y and (v1 : X implies e1 : T) and (v2 : Y implies e2 : T)
(match ι 1(x) with ι 1(v) in e1 or ι 2(v) in e2) = e1 [ x / v ]
(match ι 2(y) with ι 1(v) in e1 or ι 2(v) in e2) = e2 [ y / v ]

Like product types, we’ll make sum types variadic.

X + Y + Z ≠ X + (Y + Z) ≠ (X + Y) + Z

Although these three types are distinct, they are all, of course, isomorphic.

ι 1(x) : X + Y + Z if x : X
ι 2(y) : X + Y + Z if y : Y
ι 3(z) : X + Y + Z if z : Z

After we described product types, we described record types, which are product types distinguished by the labels of their fields even when they have the same component types. We’ll now do the same with sum types, and in fact, these are the types that feature in programming languages. I’ve never heard separate names for these two kinds of sum types (those without and those with labels).

Essentially, we’re replacing the injections “ ι 1 ”, “ ι 2 ”, ... with bespoke methods of constructions (called, straightforwardly, constructors).

extension (X + Y) = { p | p : X + Y } ≅ {  (0 , x) | x : X } ∪ {  (1 , y) | y : Y }

extension (a X + b Y) ≅ {  (a , x) | x : X } ∪ {  (b , y) | y : Y }

todo Let’s talk briefly about constructors. They’re like functions; in fact, we could even type them (relate them using has-type) as functions.

a (x) : a X + b Y if x : X
b (y) : a X + b Y if y : Y

If we need to declare the constructors a and b, we might simply write

a X + b Y : Type ,

but if we need to indicate syntactically that “ a ” is a constructor in an expression like “ a(x) ”, we’ll use the alternative syntax

⁅ a: x ⁆ : a X + b Y
⁅ b: y ⁆ : a X + b Y,

mirroring the syntax for record types.

⟨ a: x , b: y ⟩ : a X × b Y

In Rust, sum types are called “enumerated types” (and declared using “enum”), but more commonly, “enumerated type” refers to a sum type where the type of every variant is Unit.

todo Example of an enumerated type.

todo variants, discriminants

Digression: many languages use a syntax like

S : Type = C0 | C1

Here the type of each variant is Unit, and this is fine.
But when the types of the variants are not Unit, many languages use

S : Type = C1 X | C2 Y

and this is horrendous and terribly confusing because it then appears that C1 should be applied to a type, when in fact it should be applied to a value.

Slightly better is something like

S : Type = C1 (_ : X) | C2 (_ : Y)

Now Consider

S : Type = C1 (_ : X) | C2 (_ : Y) | C3 (_ : Z)
S : Type = X + Y + Z

which implies, if C1 (_ : X) is supposed to represent a collection of values, that the “ | ” operator is variadic and builds a type from two or more collections of values. But we arguably ought to be able to give some meaning to the expression (whether the same meaning or not) if it were built incrementally:

(C1 (_ : X) | C2 (_ : Y) ) | C3 (_ : Z) = (X + Y) + Z

Then the “ | ” operator takes types, as it were, and so we conclude that the expression C1 ( _ : X ) is actually a type. We could make this more explicit or precise this by introducing “labelled types”, writing ^aX rather than a ( _ : X ), and then use that to build record types and sum types.

a X : Type if X : Type
a X ≠ X
a X ≠ b X if a ≠ b
(a: x) : a X if x : X

todo Inductive types are very similar, but the type can be mentioned in its own definition.

Here is Rocq:

Inductive S : Type :=
| inl : A -> S
| inr : B -> S.

Here is Lean:

inductive S : Type where
| inl : A -> S
| inr : B -> S

(Here A and B would be concrete types previously defined.)
Also notice that the syntax used by Rocq and Lean is up front about constructors behaving like functions.

todo Rust is halfway there (types can be mentioned in their own definitions but only behind a reference or box — but I need to check this).

> Brief Aside

nominal and structural typing

Suppose we’re using this sort of syntax.

S = C1 (_ : X) | C2 (_ : Y)
s = C1(x)

Then of course

s : S

But is it also the case that...?

s : X + Y

todo Let’s briefly discuss nominal versus structural typing.

> Algebraic Data Types

todo If you have product and sum types, you have algebraic data types.

todo Complain about Haskell, which allows you to write

data Pair = Pair Int Int

so that it’s impossible to tell whether Pair refers to the type or to the constructor, and the fact that people actually do this is mildly infuriating.

> Universal Types

In Rust parlance, these are generic functions.

Λ α . e : Π α . T if α : Type implies T : Type and e : T
(Λ α . e)  [ X ] = e [ X / α ] where X : Type

Note that an instance of a universal type yields a value, not a type, when applied to an argument!

Also note that α is a metavariable standing in for a type variable rather than standing for a type.

Since universal types are more unusual than everything we’ve seen so far, an example may be expedient.

There are a few different ways to write universal types.

∀ α . T
α Type ⇒ T
Π (α : 𝒰) T
Π α . T

※ Here T is a type (an inhabitant of Type) that uses or includes α . The term T isn’t actually required to include α, but the utility of universal types is that it can.
For example, the type of

Λ A . λ x . ⟨ x , x ⟩

might written any of the following ways:

∀ A . A → A × A
A Type ⇒ (A → A × A)
Π A : 𝒰 A → A × A
Π A . A → A × A

• The first of these is standard for type systems without dependent types.
• The second resembles ordinary function types. ※ See the brief aside later in this section. Just as an instance of S → T takes a value (an instance of S ) and returns a value of type T, an instance of Type ⇒ T takes a type (an instance of Type) and returns a value of type T.
• The third is standard for type systems with dependent types, where α may be an inhabitant of something other than 𝒰 (so that T depends on a value rather than a type).
• The fourth is a hybrid of the first and third, and it’s the notation we’ll be using.

Note that using Π for non-dependent types is unusual! It’s a choice made on æsthetic grounds.

A language with universal types is called a λ2 language. The language that has only function types and universal types is called System F.

System F features impredicative quantification, meaning that terms may be applied to types that themselves contain quantifiers. An instance of a type can be applied to that same type.

Id = Π α . α → α
id : Id = Λ α . λ (x : α) . x
id [ Id ] : (Π α . α → α) → (Π α . α → α)
 = λ (x : Π α . α → α) . x
assert id [ Id ]  (id) = id

Notably, despite the fact that recursion is not possible (System F is strongly normalizing), type inference for System F is undecidable (— that is to say, some type annotations are required in order to perform type inference).

Impredicative quantification is rare in programming languages, presumably for that reason and because impredicativity makes monomorphization difficult.

todo In order to monomorphize or compile the function, do we have to examine each of its call sites? — every call site has to be visible. Otherwise, you have to have use dynamic dispatch.

As one might expect, predicative quantification means that terms may only be applied to types that do not contain quantifiers. So long as the functions are themselves not allowed to be supplied as arguments, functions that have parameters containing quantifiers are tractable in a compiled language without dynamic dispatch.

numbers : N × N × N = ⟨ 5 , 17 , 257 ⟩
colors : C × C × C = ⟨ Amaranth , Violet , Periwinkle ⟩
select-pair : (Π α . α × α × α → α) → ⟨ N , C ⟩
 = λ p . ⟨ p [ N ]  (numbers)  , p [ C ]  (colors)  ⟩
fst = Λ α . λ t . t .1
snd = Λ α . λ t . t .2
thd = Λ α . λ t . t .3
assert select-pair (fst) = ⟨5, Amaranth⟩
assert select-pair (snd) = ⟨17, Violet⟩
assert select-pair (thd) = ⟨257, Periwinkle⟩

※ The p stands for projection.
Here, static analysis of the body of select-pair alone allows us to rewrite its signature as

select-pair : p1 (N × N × N → N) × p2 (C × C × C → C) → ⟨ N , C ⟩
 = λ p1 , p2 . ⟨ p1 (numbers)  , p2 (colors)  ⟩

and now we can compile the function in isolation.
Later, we can mechanically fix up each call site accordingly.

assert select-pair (fst[ N ]  , fst[ C ] ) = ⟨5, Amaranth⟩
assert select-pair (snd[ N ]  , snd[ C ] ) = ⟨17, Violet⟩
assert select-pair (thd[ N ]  , thd[ C ] ) = ⟨257, Periwinkle⟩

We might, however, restrict ourselves further to prenex polymorphism, where quantifiers are required to appear at the beginning (at the outermost level) of a type. This is straightforwardly accomplished by classify­ing type variables, type literals, and function types as monotypes, which do not contain quantifiers, and then defining polytypes to be types that are quantified over monotypes (but not polytypes). todo Most languages with polymorphism have prenex polymorphism. (I believe this applies to Rust.)

> Type Operators

todo We’re covering this because it’ll be briefly mentioned later, but we won’t be using it for most of our discussion.

todo introduction

todo difference between the constructors of a type (“value” constructors, I suppose) and type constructors

todo difference between type constructors and type operators (Rust allows you to define new type constructors but doesn’t really have type operators?)

todo We already had several type constructors, like “×” and “→”; what we’re going to add here is the ability to define new type constructors from within the language itself.

todo example

todo We’ve omitted some of the type annotations in the example above. Type operators add a new level to our type system — we can now create functions between types and apply them to types exactly like we can create functions between values and apply them to values. Our new level is called Kind, and we have the following new typing rules:

Type : Kind
Type ⇒ Type : Kind
Λ α . T : α Type ⇒ Type if α : Type implies T : Type

or alternatively

Π α . Type : Kind
Λ α . T : Π α . Type if α : Type implies T : Type

and then

(Λ α . T)  [ X ] = T [ X / α ] where X : Type

Note that, in constrast to an instance of a universal type, an instance of Type ⇒ Type yields a type, not a value, when applied to an argument!

A language with type operators is called a λω language. The langauge that has only function types and type operators is called System Fω.

A language with both universal types and type operators is called a λω language. The language that has only function types, universal types, and type operators is called System Fω.

Lean and Rocq are a nice demonstration. Here is Lean:

inductive S (α : Type u) (β : Type v) : Type (max u v) where
| inl : α -> S α β
| inr : β -> S α β

Here is Rocq:

Inductive s (A : Type) (B : Type) : Type :=
| inl : A -> s A B
| inr : B -> s A B.

If s α β : Type , then

s : Π α , β . Type

and we might also write the following type annotations.

inl : Π α , β . α → s [ α , β ]
inr : Π α , β . β → s [ α , β ]

Here s is a type operator and inl and inr are universally quantified.

> Brief Aside

generalized function types

Ordinary function types, universal types, and type operators can be seen as specializations of a more general function type.
Suppose that X : Type and Y : Type ; then the types we’ve seen have the following shapes:

In a type system with all four, the type hierarchy collapses, erasing the distinction between types and terms that are not types (which we’ve been calling values). The language that allows all four of these is called the calculus of constructions.

> Reference Types

todo mention auto deref

> Typographic Conventions

Below is a summary of the typographic conventions we’ve been using.

⊢ Existential Types

todo flattening the inhabitants of existential types

⊢ Traits as Existential Types

Now for our first example.

IterTrait : Type = Π Output . Σ Self . state Self × next (& Self → Option Output)
ListIterator : Type = Π Item . list & List Item × index Integer
listNext : Π Item . & ListIterator Item → Option Item
 = Λ Item . λ state . if state. index < state. list . length
then procedure
 let x = state. list [ state. index ]
increment & state. index
yield Some (x)
else None
listToIterator : Π Item . & List Item → IterTrait Item
 = Λ Item . λ xs . ⟨ Self: ListIterator , state: ⟨ list: xs , index: 0 ⟩ , next: listNext Item ⟩

IterTrait : Type = Π Output . Σ Self . Self × (&mut Self -> Option Output)

ListIterator : Type = Π α . & List α × Usize

listNext : Π α . &mut ListIterator α -> Option α
  = Λ α . λ s . if s.index < s.list.length      // “s” for iterator state
                then proc
                     | let x = s.list[s.index]
                     | s.index += 1
                     | yield Some(x)
                else None

listToIterator : Π α . & List α → IterTrait α
  = Λ α . λ xs . ⟨state: ⟨list: xs, index: 0⟩, next: listNext α⟩

With the iterator object captured in a closure, the existential type is no longer required.

Iterator : Type = Π Output . Unit → Option Output
listToIterator : Π Item . & List Item → Iterator Item
 = Λ Item . λ xs . let index = Box 0 in
 λ _ . if ⭑ index < xs. length
then procedure
 let x = xs [ ⭑ index ]
increment index
yield Some (x)
else None

Iterator : Type = Π Output . Unit -> Option Output

listToIterator : Π α . & List α → Iterator α
  = Λ α . λ (xs : List α) . let mut index = Box 0 in
      λ . if index < xs.length
          then proc
          | let x = xs[index]
          | *index += 1
          | yield Some(x)
          else None

> Concluding Observation

todo summarize Rust (inductive types but with restrictions, universal types but with restrictions, type constructors but not type operators, existential types but with restrictions)