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)()
}

Impressive indeed, even if it's not fully clear whether it can work as-is with the current proposal for Go generics: as @ianlancetaylor pointed out, what's the return type of Plus ?

I guess a side question - but a very important one - is: can we get compile-time Turing completeness with a similar technique?

The current proposal for Go generics tries to steer away from it, for example by forbidding partial and full specialization of generic types and functions. I agree with such attempt to avoid it, because accidentally introducing Turing completeness at compile-time usually results in horrible syntax, but is such an enticing feature that many programmers will use it nonetheless. See C++ template metaprogramming for an example.

And it has the habit of popping up in unexpected places - as for example Conway's Game of Life

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.