This question is common enough you’ve probably heard it posed countless times: “Should my new programming language use a Hindley-Milner (HM) type system or a Bidirectional (Bidir) one?” What’s that? I need to understand friends don’t just bring up type inference in casual conversation?
OK, ouch, fair enough. But…whatever. This is my blog. We’re doing it anyway! I don’t know what you expected when you clicked on a programming languages blog.
Picking a type system is a real barrier for would be language developers. Eyes full of trepidation as they navigate the labyrinth of nuanced choice that goes into everything a programming language asks of them. Which type system to choose is just another quandary in the quagmire as they trudge towards a working prototype.
Its understandable they’d want to make a quick decision and return to marching. But this is the wrong question to ask. The question presumes that HM and Bidir are two ends of a spectrum. On one end you have HM with type variables and unification and all that jazz. On the other end you have bidirectional typing where annotations decide your types and little inference is involved. This spectrum, however, is a false dichotomy.
What folks should actually be asking is “Does my language need generics?”. This question frames the problem around what your language needs, rather than an arbitrary choice between two algorithms of abstract tradeoffs. Perhaps more importantly, it determines if you’ll need unification or not.
Generics, generally, require a type system that supports unification. Unification is the process of assigning and solving type variables. If you’ve ever seen Rust infer a type like Vec
Note We don’t have time today. But if you’re interested in how unification works, I have a tutorial about it
When facing down designing a type system, knowing if you need unification or not decides a lot for you. Unification sits center stage in Hindley-Milner. When you pick HM you pick unification.
The story is more interesting for bidirectional typing. If you look to the literature, you’ll find plenty of example of bidirectional typing without a unification in sight. By introducing annotations at key locations, you can type check sophisticated programs with no type variables. A key insight of bidirectional type is how much you can do without unification. And don’t get me wrong; it is cool how much it can do.
But this leads to the incorrect perception that bidir can’t or shouldn’t use unification. The opposite couldn’t be more true. Bidirectional typing supports all the same features as HM typing, and more, forming more of a superset relationship. Unification slots into bidirectional typing like a vim user slots into home row.
... continue reading