Constructing the Natural Numbers Using Go2 Contract

NaturalNumbers.go

// A natural number has a successor, and is a successor of zero (the peano axiomatization)
contract Natural(x T) {
	var v = Succ(x)()
	var b bool = IsZero(x)
}

type Nat(type T Natural) struct {}

type Z Nat(struct{})

func IsZero(type T)(n Nat(T)) bool {
	_, ok := n.(Z)
	return ok
}

func Succ(type T)() Nat(T) {
	return Nat(T){}
}

func Prev(type T Natural)(n Nat{T}) T {
	return T{}
}

var One = Succ(Z)() // type will be Nat{Nat{struct{}}}, where Nat{struct{}} is zero

contract Summable(x, y Natural)  {
	var n Natural = Plus(X, Y)(x, y)
}

func Plus(type A, B Natural)(a Nat{A}, b Nat{B}) Nat {
	// Zero + any number = the number
	if IsZero(a) {
		return Prev(b)
	}
	// Otherwise it's the succesor of Plus(A, B)
	var v Nat = Plus(A, B)(Prev(A)(a), B)
	// Just have to figure out if this works
	return Succ(Nat)()
}

Thank you for making this explicit! Unfortunately when you’re not defining a language in a formal and mathematical way, it might not be obvious what you’re really doing when creating a new construct. Your post helps shed light on that unintentional side-effect.