Nat.swift

// Playground - noun: a place where people can play

protocol ℕ {
	static func construct() -> Self
	static var value : UInt { get }
}

struct Zero : ℕ {
	static func construct() -> Zero {
		return Zero()
	}
	static var value : UInt {
		return 0
	}
}

struct Suc<N : ℕ> : ℕ {
	static func construct() -> Suc<N> {
		return Suc()
	}
	static var value : UInt {
		return 1 + N.value
	}
}

struct Ident<N : ℕ> : ℕ {
	static func construct() -> Ident<N> {
		return Ident()
	}
	static var value : UInt {
		return N.value
	}
}

struct Plus<N : ℕ , M : ℕ> : ℕ {
	static func construct() -> Plus<N, M> {
		return Plus()
	}
	static var value : UInt {
		return N.value + M.value
	}
}

struct Mult<N : ℕ , M : ℕ> : ℕ {
	static func construct() -> Mult<N, M> {
		return Mult()
	}
	static var value : UInt {
		return N.value * M.value
	}
}

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

func succ<N : ℕ>(n : N) -> Suc<N> {
	return Suc<N>()
}

func +<N : ℕ>(n : N, _ : Zero) -> Plus<N, Zero> {
	return Plus<N, Zero>()
}

func +<N : ℕ>(_ : Zero, n : N) -> Plus<Zero, N> {
	return Plus<Zero, N>()
}

func +<N : ℕ, M : ℕ>(n : N, m : M) -> Plus<N, M> {
	return Plus<N, M>()
}

func *<N : ℕ>(n : N, _ : Zero) -> Zero {
	return Zero()
}

func *<N : ℕ>(_ : Zero, n : N) -> Zero {
	return Zero()
}

func *<N : ℕ, M : ℕ>(n: N, m : M) -> Mult<N, M> {
	return Mult<N, M>()
}

typealias _2 = Suc<Suc<Zero>>;
typealias _3 = Suc<Suc<Zero>>;

typealias _4 = Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>
typealias _6 = Plus<Suc<Suc<Zero>>, Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>>
typealias _8 = Mult<_4, _2>

let _15 = _2() + _3() + _4() + _6()
let _30 = _15 * _2()
let _22 = _15 + succ(_6())

let mix = _30 + _2() * _3() + _15 + _22

Zahlen.swift

// Playground - noun: a place where people can play
// We're in ℤ country now

protocol ℤ {
	static func construct() -> Self
	static var value : Int { get }
}

struct Zero : ℤ {
	static func construct() -> Zero {
		return Zero()
	}
	static var value : Int {
		return 0
	}
}

struct Suc<N : ℤ> : ℤ {
	static func construct() -> Suc<N> {
		return Suc()
	}
	static var value : Int {
		return 1 + N.value
	}
}

struct Rec<N : ℤ> : ℤ {
	static func construct() -> Rec<N> {
		return Rec()
	}
	static var value : Int {
		return N.value - 1
	}
}


struct Ident<N : ℤ> : ℤ {
	static func construct() -> Ident<N> {
		return Ident()
	}
	static var value : Int {
		return N.value
	}
}

struct Plus<N : ℤ , M : ℤ> : ℤ {
	static func construct() -> Plus<N, M> {
		return Plus()
	}
	static var value : Int {
		return N.value + M.value
	}
}

struct Sub<N : ℤ , M : ℤ> : ℤ {
	static func construct() -> Sub<N, M> {
		return Sub()
	}
	static var value : Int {
		return N.value - M.value
	}
}

struct Mult<N : ℤ , M : ℤ> : ℤ {
	static func construct() -> Mult<N, M> {
		return Mult()
	}
	static var value : Int {
		return N.value * M.value
	}
}

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

func succ<N : ℤ>(n : N) -> Suc<N> {
	return Suc<N>()
}

func recc<N : ℤ>(n : N) -> Rec<N> {
	return Rec<N>()
}

func +<N : ℤ>(n : N, _ : Zero) -> Plus<N, Zero> {
	return Plus<N, Zero>()
}

func +<N : ℤ>(_ : Zero, n : N) -> Plus<Zero, N> {
	return Plus<Zero, N>()
}

func +<N : ℤ, M : ℤ>(n : N, m : M) -> Plus<N, M> {
	return Plus<N, M>()
}

func -<N : ℤ>(n : N, _ : Zero) -> Sub<N, Zero> {
	return Sub<N, Zero>()
}

func -<N : ℤ>(_ : Zero, n : N) -> Sub<Zero, N> {
	return Sub<Zero, N>()
}

func -<N : ℤ, M : ℤ>(n : N, m : M) -> Sub<N, M> {
	return Sub<N, M>()
}

func *<N : ℤ>(n : N, _ : Zero) -> Zero {
	return Zero()
}

func *<N : ℤ>(_ : Zero, n : N) -> Zero {
	return Zero()
}

func *<N : ℤ, M : ℤ>(n : N, m : M) -> Mult<N, M> {
	return Mult<N, M>()
}

typealias _2 = Suc<Suc<Zero>>;
typealias _3 = Suc<Suc<Zero>>;

typealias _4 = Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>
typealias _6 = Plus<Suc<Suc<Zero>>, Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>>
typealias _8 = Mult<_4, _2>

let _15 = _2() + _3() + _4() + _6()
let _30 = _15 * _2()
let _22 = _30 - _8()

let mix = _30 + _2() * _3() + _15 - _22