How to choose between Hindley-Milner and bidirectional typing
thunderseethe.dev
thunderseethe.dev
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"
But to the actual point of the article: 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.
Being a student is so much fun, and we often waste it, or at least don't value it as much as we ought. 20 years later I'd love to go back.
An aside, but some years ago I watched the demo 1995 by Kewlers and mfx[1][2] for the first time and had a visceral reaction precisely due to that, thinking back to my teen years tinkering on my dad's computer, trying to figure out 3D rendering and other effects inspired by demos like Second Reality[3] or Dope[4].
I seldom become emotional but that 1995 demo really brought me back. It was a struggle, but the hours of carefree work brought the joy of figuring things out and getting it to work.
These days it's seldom I can immerse myself for hours upon hours in some pet project. So I just look things up on the internet. It just doesn't feel the same...
[1]: https://www.youtube.com/watch?v=weGYilwd1YI
[2]: https://www.pouet.net/prod.php?which=25783
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.
He never actually spoke about type inference in my presence. He did teach me CCS (pi-calculus predecessor) a couple of years later, by which time I could appreciate him.
Personally I am a bit skeptical about whether complex type inference doesn't do more harm than good in some cases. A valid alternative approach is to just make type declarations required. Sure infer trivial types like when doing variable assignment but other than that just expect types to be provided. This drastically cuts down on complexity and enforces more readable programs. And it gives you much better error messages.
Or go the opposite way: If you want a language that feels dynamic and leads to prototyping, well a type system that is total and complete might be too heavy. Instead of only allowing programs that are proven to be typed correctly you might want to allow all programs that you can not proved to be wrong. Lean into gradual typing. Everything goes at first and the typing becomes as strict as the programmer decides based on how much type information they add.
Those are both very valid approach. Not every language needs that level of type inference.
When new programmer discover ML-family language, they are often stunned by how lightweight it feels, because you don't have to annotate anything. If your types are not structurally too complicated and you want something really easy to use, HM is still the nicest experience.
Naturally, it's all a tradeoff, and if you want specific features (chiefly: borrows, high-order types, overloading, or Typescript-like features), you will need to abandon complete inference (and use something like bidirectional, most likely).
If you're having trouble reasoning about how variables are unified, it's either because you never actually built a strong gut intuition for it, or it's because you're writing Very Bad Code with major structural issues that just so happen to live in the type system. In this case it's the latter. For an HM type system, 153 choice points for an expression is ludicrous unless you're doing heavy HKT/HOM metaprogramming. The type system, and more broadly unification, is a system to solve constraints. Explosive choice indicates a major logical fault, and most probably someone naively trying to use a structural type system like a nominal one and/or a bit too much unsound metaprogramming.
Thankfully of course, you can simply just specify the type and tell the compiler exactly what it should be using. But that's not really resolving the issue, the code still sucks at the end of the day.
Now higher order unification? That's an entirely different matter.
Load bearing hand waving.
If you have generics and want type annotations to type check at compile time, you are going to need unification,
let l: List<Animal> = List(dog, cat)
At that point, you have written all the machinery to do inference anyway, so might as well use it.
I guess you could have a language where the above must be gradually typed like
let l: List<Animal> = List<Animal>(dog: Animal, cat: Animal)
but that doesn't seem particularly ergonomic.
Generics and row polymorphism already cover most structural patterns. The real problem is semantic ambiguity. If algebraic types or unions are not used, the type system cannot tell meaningful differences.
For example, if both distance and velocity are just float, the compiler has no way to know they represent different things and will allow them to mix. For this to be treated as a compile time error, defining the types and sincerely using them for different semantic meanings throughout is needed.
Yes, this is the way. And if you ensure that the type system is never abused to control dispatch - i.e. can be fully erased at runtime - then a proposed language supplied with some basic types and an annotation syntax can be retrofitted with progressively tighter type-checking algorithms without having to rewire that underlying language every time.
Developers could even choose whether they wanted super-safe checking (that precludes many legal forms), or more lenient checking (that allows many illegal forms), all in the same language!
Ironically the language which needed this most was C++, which took ages to get the "auto" keyword and can still have a bit of a problem with fully expanded template names in error messages.
At least with dynamic typing you might be in a flow state and care more about the shape of data than the types so it might be valid. But in static type land, not so sure.
But yeah as I said, definitely infer trivial things like variable types based on initializing. I am more against inferring parameter and return types and the like. The auto keyword is super useful but also can be abused when overused.
It's the opposite! Type inference means you can rely on the compiler to check that everything is consistent while you just read what's in front of you. You don't need to think about types at all; the annotations would just be noise.
It simplifies reading (via not needing to care) and writing (via suggestions/auto-complete/jump-to-definition/better error messages).
You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.
https://github.com/LPTK/simple-sub
https://www.reddit.com/r/ProgrammingLanguages/comments/hpi54...
Anyway I didn't mean that simple-sub makes subtyping inference great. It (and mlsub) seems to be just better than previous approaches
As a developer I personally prefer structural subtyping, but structural subtyping is harder for a compiler to optimize runtime performance for.
Nominal sub-type hierarchies allows for members to be laid out linearly and member accesses becomes just an offset whereas a structural system always has the "diamond problem" to solve (it's hidden from users so not a "problem" but will still haunt compiler/runtime developers).
Now the kicker though, in practice nominal subtype polymorphism has other issues for performance on _modern_ computers since they create variable sized objects and cannot be packed linearly like monomorphic structures.
In the 90s when languages settled on nominal typing memory speeds weren't really an huge issue, but today we know that we should rather compose data to achieve data-polymorphic effects and singular types should be directed to packing.
Thus, most performance benefits of a nominal type system over a structural don't help much in real-life code and maintenance wise we would probably have been better off using structural types (iirc Go went there and interfaces in Java/C# achieves mostly the same effect in practice).
Example usecase: an Effect may fail with 2 types, but actually you have handled one/catched one so you want to remove it.
Elm-like HM systems handle fine, as you say it, row polymorphism mostly over records.
I'm not an expert in all of this, started studying this recently, so take my words with a grain of salt.
Bidirectional type inference is a type inference style where you traverse the syntax tree once. Sometimes the type info flows top to bottom and sometimes it flows bottom up. If your type inference algorithm works by traversing the syntax tree, I suggest reading more about bidirectional type inference to get a better idea of how to best coreograph when the type info goes up and when it goes down.
Hindley-Milner type inference works by solving constraints. First you go through the code and figure out all the type constraints (e.g. a function call f(x) introduces the constraint that x must have the same type as the argument of f). Then you solve the system of equations, as if you'd solve a sudoku puzzle. This sort of "global type inference" can sometimes figure out the types even if you don't have any type annotations at all. The catch is that some type system features introduce constraints that are hard to solve. For example, in object oriented languages the constraints are inequalities (instanceof) instead of equalities. If you plan to go this route it's worth learning how to make the algorithm efficient and which type system features would be difficult to infer.
Yes, in my language I just build code directly from syntax tree in single pass (with a couple of minor exceptions). No complex machinery for type deduction is involved. So, now I assume it's called bidirectional type inference.
Personally I find what Rust does with possibility to avoid specifying types for variables isn't that great. It allows writing code which is hard to read, since no type information is present in source code. Also I suppose that it makes compilation slower, since solving all these equations isn't so easy and computationally-cheap.
So, just to be clear, bidirectional type inference is a particular kind of machinery for type deduction (complexity is in the eye of the beholder). The defining characteristic of bidirectional type inference is that type information flows in both directions, not that it takes a single pass for type checking over the tree.
And that's, again, a single pass for type checking - the compiler as a whole can and usually does still take many passes to go from syntax tree to code. Pascal was famously designed to be compiled in a single pass, but it doesn't have any type inference to speak of.
It doesn't mean you have to use an advanced one, but your choice choose be based on knowledge, not ignorance.
A lot of harm; including the billion dollar mistake, has been done by badly designed type systems from the Java/C/C++ family.
..because that is more practical.
Unification is simple, not very hard to implement and more powerful. Bidir gives better error messages and is more "predictable".
I personnaly lean strongly towards unification. I think you can get good enough error messages and what you lose with bidir is not worse it. But clearly the Rust core team disagreed. They clearly don't mind annotations.
Anyway, here is my non answer: it's a trade off.
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.
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.
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.
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.