The Easiest Way to Build a Type Checker

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.

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.

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));
    }

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)

Type annotations on functions in Haskell (or similar languages) are useful for:

1. leveraging the type checker to verify (aspects of) the correctness of your function, and

2. communicating intent to humans

I've found in my own explorations with Haskell that its useful to write with functions with them, then verify that they work, and then remove them to see what the inferred would be (since it already compiled with the annotation, the inferred type will either be identical to or more general than the previously declared type), and generally (because it is good practice to have a declared type), replace the old declared type with the inferred type (though sometimes at this point also changing the name.)

what if your IDE can show the type of any expression as a tooltip ? Would you still think the same?

> I think it's pretty widely agreed that requiring type annotations at the function level is a good thing anyway. Apparently it's considered good practice in Haskell even though Haskell doesn't require it.

In Haskell-land: At the global scope, yes, that's considered good practice, especially if the function is exported from a module. When you just want a local helper function for some tail-recursive fun it's a bit of extra ceremony for little benefit.

(... but for Rust specifically local functions are not really a big thing, so... In Scala it can be a bit annoying, but the ol' subtyping inference undecidability thing rears its ugly head there, so there's that...)

No, HM is unification based and requires no annotations at all.