Rust Traits as Existential Types

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

Systems 1a, 1b, and 1c use a single λ2 (System F ) or λω (System Fω) language endowed with existential types, but system 2 uses a separate metalanguage and language. We don’t actually need anything near the full power of System F – just predicative polymorphism.

todo warmup with universal types

Now for our first example.

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

makeListIterator : Π α . & 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

makeListIterator : Π α . & 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

Demonstration

This section is to test formatting; the actual content is incorrect, so don’t give it any attention.

1a Type-theoretic Notation

let myTrait : Type = ∃ α, β . (α -> β) × (α -> unit)

let myFoo : &str -> u32  = λ x . /* ··· */
let myBar : &str -> unit = λ x . /* ··· */

let myImpl : myTrait = ⟨&str, u32, ⟨myFoo, myBar⟩⟩

let s : &str = “helo”
let u : u32 =
  let ⟨α, β, ⟨foo, bar⟩⟩ = myImpl in foo(s)

let myUse : myTrait -> (??? -> unit) =
  λ ι . let ⟨α, β, ⟨foo, bar⟩⟩ = ι in λ x . /* ··· */

let Clone : Type = ∃ α . Ref(α) -> α

let cloneFunc : ∀ α . Ref(α) -> α
  = Λ α . λ x . /* ··· */

let cloneImpl : ∀ α . Clone
  = Λ α . ⟨α, cloneFunc(α)⟩


let u16CloneImpl : Clone = cloneImpl(u16)
let u32CloneImpl : Clone = cloneImpl(u32)
let u64CloneImpl : Clone = cloneImpl(u64)

1b Hybrid Notation

let myTrait : Type = exists(α, β){
  {Self: α, Assoc: β, foo: α -> β, bar: α -> ()}
}

let myFoo : &str -> u32 = lambda(self) { /* ··· */ }

let myBar : &str -> () = lambda(self) { /* ··· */ }

let myImpl : myTrait = {
  Self:  &str,
  Assoc: u32,
  foo:   myFoo,
  bar:   myBar
}

let s : &str = “helo”
let u : u32 = compiler::get_implementation(myTrait, &str).foo(s)

let myUse : TODO = lambda(α) {
  let i : myTrait = compiler::get_implementation(myTrait, α)
  lambda(x) {
    let (Self, Assoc, foo, bar) = (i.Self, i.Assoc, i.foo, i.bar);
  }
}

let Clone : Type = exists(α) {
  {Self: α, clone: &α -> α}
}

let cloneFunc : forall(α){&α -> α} = lambda(α) {
  lambda(self) {
  }
}

let cloneImpl : forall(α){Clone} = lambda(α) {
  {Self: α, clone: cloneFunc(α)}
}

let u16CloneImpl : Clone = cloneImpl(u16)
let u32CloneImpl : Clone = cloneImpl(u32)
let u64CloneImpl : Clone = cloneImpl(u64)

1c Rust-like Notation

trait myTrait = struct {
  Self  : Type,
  Assoc : Type,
  foo   : fn(Self) -> Assoc,
  bar   : fn(Self)
};

fn myFoo(self : &str) -> u32 { /* ··· */ }

fn myBar(self : &str) { /* ··· */ }

let myImpl : myTrait = {
  Self:  &str,
  Assoc: u32,
  foo:   myFoo,
  bar:   myBar
};

let s : &str = "helo";
let u : u32 = s.foo();  // Or u = &str::foo(s)

fn myUse<T : myTrait>(x : T) { /* ··· */ }


trait Clone = struct {
  Self  : Type,
  clone : &Self -> Self
};

fn cloneFunc<T>(x : &T) -> T { /* ··· */ }

fn cloneImpl<T>() -> Clone
{
  return {
    Self:  T,
    clone: cloneFunc<T>
  };
}

let u16CloneImpl : Clone = cloneImpl(u16);
let u32CloneImpl : Clone = cloneImpl(u32);
let u64CloneImpl : Clone = cloneImpl(u64);