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

The "interesting" construct above is intended to showcase the similarity between dependent types and go contracts. This example mirrors Idris's Running example: Addition of Natural Numbers.

I'm not advocating for dependent types in Go, but rather noting the similarity as "food for thought". Certain aspects of dependent typing may be useful to Go, or we may want to intentionally steer away from such capabilities. I found it useful to consider this:

Paramterized types are a type's constructors and formation rules and contracts are a types elimination and computation rules.

I'm confused by the result type of Plus. It can't just be Nat, because Nat requires a type argument. But what would the type argument be?

I think you cannot do this.
From the draft:

The body of a contract may not refer to any name defined in the current package. This rule is intended to make it harder to accidentally change the meaning of a contract. As a compromise, a contract is permitted to refer to names imported from other packages, permitting a contract to easily say things like “this type must support the io.Reader interface:”

Using only features of Go1, we can already model natural numbers:

type Nat interface {
	Plus(Nat) Nat
}

type zero struct{}
type suc struct{ n Nat }

var (
	Zero  = zero{}
	One   = suc{Zero}
	Two   = suc{One}
	Three = suc{Two}
)

func (_ zero) Plus(n Nat) Nat { return n }
func (m suc) Plus(n Nat) Nat  { return suc{m.n.Plus(n)} }

playground: overengineered full example.

The example shows that Go currently already supports supports function overloading, though we don't call it that way. However, we cannot do function overloading one would normally do:

func add(i,j int) int {
	return i+j
}
// won't compile: "add redeclared"
func add(i,j float32) float32 {
	return i+j
}

Yet, the natural number implementation using type Nat interface shows that we can use function overloading at the receiver.

Could this kind of function overloading introduce problems in combination with generics? Here is some hypothetical Go2 code with generics:

type Nat(type T) struct {T}

type zero struct{}
type suc struct{ n Nat }

// I write Nat(_) to mean Nat(T) for any T

func (_ Nat(zero)) Plus(n Nat(_)) Nat { return n }
func (m Nat(suc)) Plus(n Nat(_)) Nat  { return ... }

• Could this example evolve to endanger the “dual-implementation” constraint?
• Will the public interface of this implementation be not useful because of the exported Plus functions? To decide which Plus function to call on a Nat(T), one needs to decide based on T, either T=zero or T=suc. Both, zero and suc are not exported publicly.
• What about compiler optimization? zero.Plus(zero) is equal to zero. Can the compiler infer this optimization? Can the compiler infer this optimization if zero was a public constant and zero.Plus(zero) occurs outside of the current compilation unit?

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.