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.