Mind blown today: Constraint generation + solving is *not* a requirement for implementing Hindley-Milner type checkers — metavariables + unification is enough!
Conversation
Milner’s original paper agrees with you: homepages.inf.ed.ac.uk/wadler/papers/
1
9
Yeah, so it seems! Thanks for the link!
For some reason I had got it into my head that it was required, probably due to it appearing a bunch in tutorials. Apparently a lots of people on the PL discord I'm on were similarly surprised.
Quote Tweet
Sadly constraint generation + solving has been a significant stumbling block for me when learning to implement type inference over the years. It shows up in many tutorials about type checking, which had led me to think it was somehow necessary for implementing it!
Show this thread
1
4
I'd probably be able to handle using constraints in type checking now, but it was always a decent hurdle to face it when just getting into implementing programming languages, and wanting to implement something with a bit of inference – hence why I got into bidirectional typing.