At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so:
return x; Z => x
var x; Z => let x = undefined in Z
x = y; Z => let x = y in Z
if x then T else F; Z => if x then { T; Z } else { F; Z }
Since I’m starting from general type information and trying to deduce more specific types, the natural choice is refinement types. For example, the conditional operator returns a union of the types of its true and false branches. In simple cases, it works very well.
I ran into a snag, however, when trying to infer the type of the following:
function g(f) {
var x;
x = f(3);
return f(x);
}
Which is rewritten to:
\f.
let x = undefined in
let x = f 3 in
f x
HM would infer $\mathtt{f} : \mathtt{Int} \to \mathtt{Int}$ and consequently $\mathtt{g} : (\mathtt{Int} \to \mathtt{Int}) \to \mathtt{Int}$. The actual type I want to be able to infer is:
$$\mathtt{g} : \forall \tau_1 \tau_2. \:(\mathtt{Int} \to \tau_1 \land \tau_1 \to \tau_2) \to \tau_2$$
I’m already using functional dependencies to resolve the type of an overloaded + operator, so I figured it was a natural choice to use them to resolve the type of f within g. That is, the types of f in all its applications together uniquely determine the type of g. However, as it turns out, fundeps don’t lend themselves terribly well to variable numbers of source types.
Anyway, the interplay of polymorphism and refinement typing is problematic. So is there a better approach I’m missing? I’m currently digesting “Refinement Types for ML” and would appreciate more literature or other pointers.
