The Easiest Way to Build a Type Checker

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 recently implemented a Hindley Milner type checker. The algorithm itself is not necessarily super difficult (once you get your head around it ofcourse) but the way it is explained is. It seems like HM is mostly explained by people with a mathematics background that already know the proper notation. I wonder how much overlap there is between people that know the notation and do not know how HM works, probably not much.

Anyway nice demo. Bi-directional is already quite powerful!

In the small example type checker given, would a function of type A -> B -> C be represented something like this?

    { kind: "function", arg: A, returnType: { kind: "function", arg: B, returnType: C}}

EDIT:

I just noticed the working demo at the bottom that includes an example of a multi-argument function so that answers whether it works.

I grabbed the code from the article and annotated it with the different cases from the famous picture*

  switch (expr.kind) {
    case "number"/"string"/"var":
      ... [Var]
    case "call":
      ... [App]
    case "function":
      throw new Error("...[Abs]")
    case "let":
      ... [Let]

* https://wikimedia.org/api/rest_v1/media/math/render/svg/10d6...

I recently made a toy type checker for Python and had a lot of fun.

https://austinhenley.com/blog/babytypechecker.html

Nice! 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.

I've also worked with OCaml code that didn't do it and you lose a lot of the advantages of static typing. Definitely worse.

Rust got it right.

I thought the implementation here was how hindley Milner worked? I guess not?