TypeAlgebra.swift

protocol Nat { init() }
struct Zero : Nat {}
protocol NonZero: Nat { typealias Pred: Nat }
struct Succ<N : Nat> : NonZero { typealias Pred = N }

typealias One   = Succ<Zero>
typealias Two   = Succ<One>
typealias Three = Succ<Two>
typealias Four  = Succ<Three>
typealias Five  = Succ<Four>
typealias Six   = Succ<Five>
typealias Seven = Succ<Six>
typealias Eight = Succ<Seven>
typealias Nine  = Succ<Eight>

struct AddOne<N : Nat> {
  typealias Result = Succ<N>
}
struct AddTwo<N : Nat> {
  typealias Result = Succ<AddOne<N>.Result>
}
struct AddThree<N : Nat> {
  typealias Result = Succ<AddTwo<N>.Result>
}
struct AddFour<N : Nat> {
  typealias Result = Succ<AddThree<N>.Result>
}
struct AddFive<N : Nat> {
  typealias Result = Succ<AddFour<N>.Result>
}
struct AddSix<N : Nat> {
  typealias Result = Succ<AddFive<N>.Result>
}
struct AddSeven<N : Nat> {
  typealias Result = Succ<AddSix<N>.Result>
}
struct AddEight<N : Nat> {
  typealias Result = Succ<AddSeven<N>.Result>
}
struct AddNine<N : Nat> {
  typealias Result = Succ<AddEight<N>.Result>
}

protocol Binary {
  typealias A : Nat
  typealias B : Nat
}

struct Op<E0: Nat, E1: Nat> : Binary {
  typealias A = E0
  typealias B = E1
}

struct EQ {}
struct GT {}
struct LT {}

extension Binary where A == B {
  var sub: Zero { return Zero() }
  var com: EQ { return EQ() }
}
extension Binary where A == Succ<B> {
  var sub: One { return One() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<B>> {
  var sub: Two { return Two() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<B>>> {
  var sub: Three { return Three() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<B>>>> {
  var sub: Four { return Four() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<Succ<B>>>>> {
  var sub: Five { return Five() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<Succ<Succ<B>>>>>> {
  var sub: Six { return Six() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<Succ<Succ<Succ<B>>>>>>> {
  var sub: Seven { return Seven() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<B>>>>>>>> {
  var sub: Eight { return Eight() }
  var com: GT { return GT() }
}
extension Binary where A == Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<B>>>>>>>>> {
  var sub: Nine { return Nine() }
  var com: GT { return GT() }
}
struct Neg {}
extension Binary {
  var sub: Neg { return Neg() }
  var com: LT { return LT() }
}