thunderseethe

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!

What are you calling bidir, if the introduction of unification means its no longer bidir?

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

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 more about query based compilers as a concept, I highly recommend ollef's aritcle: https://ollef.github.io/blog/posts/query-based-compilers.htm...

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

> The real question is unification vs bidir

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.

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

There's an interactive playground to show off the LSP we implement at https://thunderseethe.dev/making-a-language

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 .

Take a look at The Rapier in GHC: https://www.researchgate.net/publication/220676611_Secrets_o...

It employs a similar idea. Track the set of in scope variables and use them to unique variables on collision.

Lowering our typed base AST into a System-F based IR

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

I think rather than at odds with without.boats is saying, this is very much aligned with what they are suggesting. While not literally `use A::impl std::hash::Hash for i32` is for all intents and purposes naming the impl.

Similarly, `HashMap<i32 + A::impl Hash, V>` is what they are talking about when they refer to parameterizing code on the impl chosen.

That ones on me. I blog as a way to practice writing, and right now I'm working on picking more interesting verbs.

I have a usage of `proselytize` later on that is outright smarmy.

Great write up, and you're absolutely right that implicits are moving towards ML modules. Quite possibly a production system would end up being synonymous with ML modules out of the need for named impls.

Small nit in terminology, the implicits described are coherent. Part of their value over previous implicit work is that they are coherent and stable. I have generally seen the property you're referring to called canonicity, which they do lack.

It's also custom logic to embed the code snippets within the article, they're all working code that gets pulled in from rust files. Really stellar stuff.

Damn I love this article, what a cool series of words to say.

And I wrote it, so you know it must be true!

Absolutely! That's what I'm attempting this time. I'm hoping if I start with literally just the lambda calc + integer literals I can get something working e2e and layer stuff on top from there

This captures exactly the sentiment I was trying to express.

Thanks for chiming in!