Generic method: type inference

Question

I am developing a verifier for the ActionScript 3 language and I have gone through implementing one before for my personal language.

I had a type inference limitation with the following construct:

package {
    public class C1 {
        public function f.<T>(callbackFn: () => T): void {}
    }
}

const o = new C1;
o.f(() => 10); // Error: `o.f` must be argumented
o.f.<Number>(() => 10); // Successful

I was using sort of a bidirectional type checking, where solving an expression was given a context with an "expected type" or none, such as in:

enum E {
    const M1;
}
const e: E = "m1"; // Successful
const e: E = "m2"; // Error: "m2" is not a known member

If a type annotation was missing, an expression would be resolved with no expected type and its resolved type determined the type of a binding:

const x = 10;

Most of my expectations were meet, except for the above o.f.<T>() case, where I wanted to be able to omit the .<T> list. Is this possible with my previous model or do I have to do something different?

Answer 1

If you want to stick with bidirectional checking, you could try implementing the system presented in Complete and easy bidirectional typechecking for higher-rank polymorphism (pdf). To my knowledge, AS3 doesn’t support parametric polymorphism at all (the unusual .<T> syntax is only used with the Vector class and nothing else), so I assume this is a question about your “personal language”. Given your example, I suspect you don’t actually need the “higher-rank” part—the example only needs rank-1 polymorphism—but the linked paper’s presentation is exceptionally clear and thorough, and the system would not be substantially simpler if restricted to rank-1.

In general, parametric polymorphism can be challenging to handle using local type inference schemes, including bidirectional typechecking. The “complete and easy” paper is one of the best approaches I’ve seen, but it still requires annotations on bindings of polymorphic type. Crucially, however, it does not require annotations on uses of polymorphic definitions, so it is able to handle the example in your question.

While clever, the approach is not magic: it requires the addition of a mutable context of “solver variables” representing unknown types that are incrementally instantiated as the typechecker traverses the program. This mechanism effectively adds a small amount of nonlocal type inference to an otherwise local system. However, the system does not require full unification, which distinguishes it from global inference schemes such as Hindley–Milner.