Yeah I was just wrong here. I was under the impression clang had a concept of a request the same way Swiftc does and that is just not true. That's my bad!
It is a double edged sword of the single page layout that you really have to make one point briefly and get out of there. I had to pare down many details to fit the layout.
If you want to learn how to implement a query based compiler, I have a tutorial on that here: https://thunderseethe.dev/posts/lsp-base/ (which I also highly recommend but that might be more obvious since I wrote it)
In general I agree with what youre advocating for. Languages should require annotations on function parameters and return types and most top level definitions. But even if you only infer types locally you'll still want unification to do it well. Without unification local inference will hit annoying edge cases where you have to add otherwise unnecessary annotations
Quite the opposite, imo. Unification does not exclude bidir and the two fit together very well. You can have one system with both Unification and bidir and get all the advantages of both.
Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others.
But, I maintain that what the article calls HM is trully unification independantly of what's above. This is not about algorithm W. It's actually about the tension between solving types as a large constraint problem or using annotations to check.
> You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification.
Could you expand on this? I do not follow. You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. It is not often done because people are coming around to the idea that global type inference causes spooky action at a distance, but nothing prevents it from working.
> I maintain that what the article calls HM is trully unification
In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck.
> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml.
There is no more bidir if you do that. It's just plain unification.
> In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck.
You can't implement HM without unification but you can do unification which is not HM. Actually a lot of what people call HM is not really HM but evolution of it and sometimes significant evolution.
> I wonder if this is a reference to "I need you to understand that people don't have conversations where they randomly recommend operating systems to one another"
It is!
> my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference might become undecidable
There are! Afaik most languages end up with a bidirectional system in practice for this reason. Haskell started out HM and has shifted to bidir because it interacts better with impredicative types (and visible type applications). Bidir can handle fancy features like subtyping and all sorts of nifty stuff.
This is probably my biggest regret with this article. Much earlier and much more prominently I should've explained that the title is a play on a running joke Andreas Rossberg includes in a couple of his talks "wasm does not stand for webassembly", poking fun at how they named it that to get funding, but always intended it for a more general use case.
I have a nod to it, as you point out, but I think its buried so far beneath the fold most folks have checked out and written it off by then. Live and learn .
Implicits are motivated, atleast in part, by a desire to improve upon this baseline. In the world of ML modules this is the current state. Typeclasses (as modules) have to be passed everywhere they're used explicitly and it's exhausting. I think with implicits you can keep that as a baseline but provide an implicit mechanism atop it to remove a lot of the obvious boilerplate for a win-win
