PhantomType_NatualNumber.swift

// A swift implementation of [this presentetion](https://www.slideshare.net/AkinoriAbe1/aja-2016623). 

protocol Trait {}
enum Z: Trait {}
enum S<N: Trait>: Trait {}

struct Nat<N: Trait>: CustomStringConvertible {
    let n: Int

    fileprivate init(n: Int) {
        self.n = n
    }

    var description: String {
        return String(describing: n)
    }
}

extension Nat where N == Z {
    init() {
        self.init(n: 0)
    }
}

let zero = Nat<Z>()

func succ<N: Trait>(n: Nat<N>) -> Nat<S<N>> {
    return Nat<S<N>>(n: n.n + 1)
}

func pred<N: Trait>(n: Nat<S<N>>) -> Nat<N> {
    return Nat<N>(n: n.n - 1)
}

let x = pred(n: succ(n: zero)) // x is 0 (Nat<Z>)

pred(n: succ(n: zero))
// let y = pred(n: zero) type error (zero is not Nat<S<Z>> type)
// zero == succ(n: zero) type error (zero is N<Z> type, but succ(n: zero) is N<S<Z>> type)