Mind blown today: Constraint generation + solving is *not* a requirement for implementing Hindley-Milner type checkers — metavariables + unification is enough!
Conversation
Replying to
After a bit of digging by , it seems like one reason the approach of generating constraints was introduced was as a way to improving error messages. See “Generalizing Hindley-Milner Type Inference
Algorithms”, for example: cs.uu.nl/research/techr
1
1
9
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!
1
1
5
According to , constraint generation can also stop working for dependent type checking, as problems can pile up exponentially. Instead we should aim to get rid of unsolved problems as fast as possible.
1
3
Thanks for clearing up my original misconception! If you want to see some examples of implementing type inference for dependent types I highly recommend checking out Andras' elaboration-zoo repository:
2
18
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
Show replies
Replying to
I'm partial to compositional typechecking for HM:
1
2
Oooh, interesting! Is this based on some research? I looked at the README but couldn't see anything mentioned.
1
Show replies
Replying to
Huh, meanwhile this hadn't even occurred to me as a possible misconception. (Probably because I learned a lot of this stuff from András in the first place - lucky me!)
2
1
Heh, yeah, I think I've had to piece a bunch of stuff together over the years when teaching myself stuff, and so stuff like this can creep in. I'm pretty sure a bunch of folks on the /r/ProgrammingLanguages discord were similarly surprised!
1
1
Show replies
Show more replies