I have not looked into the HM algorithm much, but is there (an educational or performance wise) advantage over implementing a (dumb) SAT solver and expressing a problem as a SAT problem? It always seemed like the "natural representation" for this kind problem to me. Does knowing that these are types _specifically_ help you somehow / give you some unique insights that won't hold in other similar SAT problems?
I suspect you've intentionally phrased this to avoid referencing type checking in particular, since this is also the main reason that mainstream programming languages tend to use hand-written parsers rather than generators from what I understand, and I imagine it applies to a lot of other features as well.
how would you encode a program like
function f<T>(x: T) { return x; }
function g(x: number) { return { a: f(x), b: f(x.toString()) }; }
if that's easy, how about length and f in:
function append<T>(xs: list<T>, ys: list<T>) {
return match xs {
Nil() -> ys,
Cons(hd, tl) -> Cons(hd, append(tl, ys)),
};
}
function flatten<T>(xs: list<list<T>>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> append(hd, flatten(xs)),
};
}
function map<T, U>(f: (T) => U, xs: list<T>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> Cons(f(hd), tl),
};
}
function sum(xs: list<number>) {
return match xs {
Nil() -> 0,
Cons(hd, tl) -> hd + length(tl),
};
}
function length<T>(xs: list<T>) { return sum(map((_) -> 1, xs)); }
function f<T>(xs: list<list<T>>) {
return length(flatten(xs)) === sum(map(length, xs));
}
If you have a bound on the size of the largest type in your program, then HM type inference is linear in the size of the program text.
The intuition is that you never need to backtrack, so boolean formulae (ie, SAT) offer no help in expressing the type inference problem. That is, if you think of HM as generating a set of constraints, then what HM type inference is doing is producing a conjunction of equality constraints which you then solve using the unification algorithm.
For a bounded size of types of sub-expressions, HM inference is quasi-linear in the size of the program, because the constraints appearing in the HM algorithm are only equality between meta-variables.A NP-complete SAT solver is not really a good fit for this kind of simple constraints. Even more so when typechecking often represents a significant part of compilation time.
(Of course the tricky part of the definition above is that the size of types can theoretically be exponential in the size of a program, but that doesn't happen for programs with human-understandable types)
Keep in mind one of the most important attributes of a good compiler is clearly explaining to the user what caused compilation failure and why. If you try to solve in a very abstract and general space it could be challenging to give an actionable error message.