Implicit interfaces

Apologies in advance if this has been thought of, and note it may be complex and a stupid idea. But I thought I'd raise the idea anyhow ...

A fellow was once baffled how to explain why the speed of light in January was the same as in July, given light is a wave and the Earth is moving through the Ether in the opposite direction in these months. Unable to sleep, he decided on a simple but revolutionary course of action: he would throw out all of Physics and just assume the speed of light was constant as an axiom, and work out the consequences from there.

Another team at Facebook, facing the huge problem of memory leaks and crashes in C and Javascript as well, discovered a new tool called Separation Logic which can be used to prove modification of a pointer variable in part of the heap cannot impact the reachability of some other part of the heap. The problem was, their source languages were pretty brain dead and the function interfaces carried no information which would allow them to prove memory safety.

So, being geniuses, they followed Albert, and simply assumed a function was memory safe, and asked instead the question backwards: what properties of the interface would be required to prove their conclusion? Of course this ripples backwards through call chains right to the root main function, as a set of precondition that must be obeyed for their proofs to hold, and that is where the checking is done.

Now consider a Chapel generic function. We cannot type check the function at the moment but we would surely like to! So .. following the examples above we simply assume the function is type correct! We work backwards and say, for this function call on a generic argument in the function, what is the type of the function making that call? The answer is polymorphic but that is fine. We do this for all dependent names in the function encoding, and then we ADD all those polymorphic functions needed to the function interface. And I mean Interface as in a Chapel Interface.

So now, we have a type safe function which is made type safe by implicitly adding an interface constraint, and we can chain backwards. If another generic calls this function, we compute its implicit interface the same way, only now, we also add the interface from the point of call to the first function we processed.

The buck stops when we find a non-generic function calling a generic function. Now we can actually try to find a set of functions needed to implement the implicit interface needed to make the whole call chain go through.

The idea has an impact on the notion of point of call as well. When a non-generic function A.f calls a generic function B.g the point of call is in module A inside f. But what is the point of call, if the function g inside module B, then calls another generic function C.h? It doesn't make sense for the POI to be in module B, so the functions needed for C.h to work come from B.

With the implicit interface idea, the POI for ALL the generic functions is A.

In more detail, this is not quite the case. The POI is not coupled with the fact a generic function is called (I think Chapel gets this wrong but I'm not sure). It is coupled with the point where a type variable is specialised. So if a generic function k calls j, and fixes one type variable but not the other, the names dependent on the first type variable can now be resolved, but those dependent on the second one can't: these have to propagate further UP the call chain to find the instantiation point.

Even this is pretty messy because a type variable can be partially specialised! What do we do then? This is important because, a polymorphic function which is in scope can be applied to a type variable, resolving it, even though the name is dependent.

So the advantage of the working backwards idea, is that you are specialising UP the call chain you resolve what you can as you can, and such resolution removes a function from the implicit interface. The only really tricky thing is recursion.

There's one further extension. The idea a function is generic or not is .. well rubbish. I had to throw that in somewhere :slight_smile:

Instead ALL functions are uniformly treated as generic and we ask instead what type variables are needed to be fixed to monomorphise the function (the answer for a non-generic function would be 0 of course). However, even a call inside a non-generic function to a non-generic function might be unresolved .. so we could actually just pass that up the call chain. So if for example, a function f contains a call to g applied to an int and there is no g in sight accepting an int .. it doesn't matter. We just add an Interface constraint that a function g with argument type int is needed. The interface has 0 generics but that is just another number.

So now, the only possible type error is in the top level function, not having access to an implementation of the implicit interface passed up from the whole program tree.

Anyhow I just thought I throw in the idea that perhaps there is a way to type check generic functions when they're seen by the compiler after all. Maybe it will inspire something that can actually work.

BTW: although the amount of data needed to be carried in an implicit interface is significant, each generic function only has to be processed once. In a descending instantiation model, you have to type check every instantiation when the type variables are fixed. So the model above is actually linear in the program size, with the same performance as real parametric polymorphism .. because .. the algorithm turns a rubbish generic into a genuinely parametrically polymorphic function with constraints. You still have to expand all the combinations for a monomorphic back end, but at least the type checking can be done linearly.