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

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⟩⟩

// TODO example of use

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
}

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

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