Thanks @robrix and CodaFi_ for the discussion :D

TypeNats.swift

// this is a playground
protocol Nat {
  class func construct() -> Self
  class func value() -> Int
}

struct Z : Nat {
  static func construct() -> Z {
    return Z()
  }
  static func value() -> Int {
    return 0
  }
}

struct S<N: Nat> : Nat {
  static func construct() -> S<N> {
    return S()
  }
  static func value() -> Int {
    return 1 + N.value()
  }
}

// how about type level bools

protocol BOOL {
  class func value() -> Bool
}

struct TRUE : BOOL {
  static func value() -> Bool {
    return true
  }
}

struct FALSE : BOOL {
  static func value() -> Bool {
    return false
  }
}

// you saw identity before

func refl<N: Nat>(n: N) -> N {
  return n
}

let twoEqualsTwo: S<S<Z>> = refl(S<S<Z>>())

// now succ, given X, give me S<X>

func succ<N: Nat>(n: N) -> S<N> {
  return S<N>()
}

let twoSuccThree: S<S<S<Z>>> = succ(S<S<Z>>())

// cool, what about less than or equal?

func sub1<N: Nat, X: Nat>(proof: N -> S<X>)(n: N) -> X {
  return X.construct()
}

// try to type it another way. you can't

let twoSubOne: S<Z> = sub1(refl)(n: S<S<Z>>())

twoSubOne // not a lie

// x less than y, needs some more type constraints... but compiler bugs exist.
// im cheating here a little.

func lessThan<N: Nat, M: Nat>(proof: M -> N)(n: N)(m: M) -> TRUE {
  return TRUE()
}

// is 2 less than 1?

let onelessthantwo = lessThan(sub1(refl))(n: S<Z>())(m: S<S<Z>>())

let zerolessthantwo = lessThan(sub1(sub1(refl)))(n: Z())(m: S<S<Z>>())


// now something useful

struct MVec<A, L: Nat> {
  let vec: Array<A>
  func index<I: Nat>(i: I, n: S<I> -> L -> TRUE) -> A {
    return vec[I.value()]
  }
}


// you must provide a proof that an index is inside the bounds of the array
let v1: MVec<String, S<S<S<Z>>>> = MVec(vec: ["hello", "rob", "rix"])
v1.index(Z(), lessThan(sub1(sub1(refl))))
v1.index(S<Z>(), lessThan(sub1(refl)))
v1.index(S<S<Z>>(), lessThan(refl))
//v1.index(S<S<S<Z>>>(), lessThan(refl)) // type error, 3 > 2

Oh they’re numbers I get it.