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.

1a Type-theoretic Notation

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

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

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

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

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

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

// We could instead use the notation
//   cloneImpl : α => Clone
// to mirror function types.

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

1b Hybrid Notation

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

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

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

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

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

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

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

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

1c Rust-like Notation

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

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

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

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

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

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

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

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