by thomasikzelf
0 subcomment
- 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!
- I recently made a toy type checker for Python and had a lot of fun.
https://austinhenley.com/blog/babytypechecker.html
- 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]
Looks like most of the hard work's done, and probably wouldn't be too tricky to get [Abs] in there too!* https://wikimedia.org/api/rest_v1/media/math/render/svg/10d6...
- 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}}
Or is that case simply not covered by this bare-bones example? I can't parse the code well enough just in my mind to tell if that would work, but I think it would work?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 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?
- 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?
Hacker News