I can try. Maybe not a real stab, but maybe a little explanation. So this cooperation, I should say, happened because Rob Pike actually reached out to Phil Wadler. They knew each other from way back, and Phil Wadler was interested, and then we started talking with Phil Wadler and with Rob Pike… He didn’t really have time to produce a beta in this, but then Phil Wadler, Ian Taylor and I started talking about what we wanna do… And they have, of course, a strong background in type theory. Phil Wadler has done this – not the same work, of course, but similar work, many years ago, for Java, so he’s really an expert.
[00:07:56.20] So now we have a whole team – it’s not just him – that have been working on this Featherweight Generic Go… Which is based on Go, but very much slimmed down. So we now have a language that really only has type declarations and methods. And those type declarations are only interfaces and only structures (structs), and the only thing you can have is methods and interfaces, of course, and methods associated with structs… And inside those methods you can only have basically single functional expressions. So it’s a very, very simplified language, but what you can do is you can invoke a method.
In this paper, he explores two situations this Featherweight Go, which is like the basic Go, simplified Go, without any generics [unintelligible 00:08:45.28] which is that basic, simplified Go, extended with generic features. And those generic features are very much modeled along the draft design, with the exception of type lists. So those type parameters, as in the draft design – the type parameters have what in the paper is called type bounds (we call them now constraints), and there are interfaces, there are also interfaces in the paper, and they basically model in a very simplified fashion what the design draft is trying to do with real Go.
The goal of this paper is to prove, first of all, that this is a sensible design, in the sense that the type system that we’re creating here is sound; you cannot create situations where you could write a program that would be unsound in terms of the type system. And then also, they tried to prove and have proven that it is possible to translate such a simplified generic Go program into a regular Go program, through a process which is called monomorphization, basically expanding everything for every possible instantiation of these generic functions and types… And then they prove that these programs are basically [unintelligible 00:10:06.22]
That’s the gist of this paper, and this gives us very strong confidence that they’re a) not designing somewhere into the blue, and b) that what we’re designing actually makes sense from a type system point of view. We’re not gonna hopefully find problems down the road, where we have some internal inconsistency. So I think that’s really the benefit…
I think it really helped us also understand a little bit better what it means to have interfaces as constraints, and how we need to type-check this. So I think there is a real synergy here.