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 language, but system 2 uses a separate metalanguage and language.

todo warmup with universal types

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 . () -> Option Output

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

listNext : Π α . &mut ListIterState α -> 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 α → Iterator α
  = Λ α . λ xs . let mut index = Box 0 in
      λ . if index < xs.length
          then proc
          | let x = xs[index]
          | *index += 1
          | yield Some(x)
          else None

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) = // TODO how is this typed?
  λ ι . let ⟨α, β, ⟨foo, bar⟩⟩ = ι in λ x . /* ··· */

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

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

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

// We could instead use the notation
//   cloneImpl : α => Clone
// to mirror function types.
// TODO move this comment to the warmup

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

// TODO point out where Rust performs automatic lookup
//   and automatic implementation

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
}

// The compiler looks up our implementation automatically.
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) { /* ··· */ }

// Alternatively,
//   fn myUse<T>(x : T) where T : myTrait { ... }

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);