How to choose between Hindley-Milner and bidirectional typing • Hacker News Board

Re: How to choose between Hindley-Milner and bidirectional typing

#31

Post by thechao » Thu, Feb 19, 2026, 12:47 PM UTC

Drup wrote: post #23

cardanome wrote: post #20

Does your language even need (complex) type inference? 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 rea…

HM is not complex type inference. In fact, among all the approaches you cite, it leads to the simplest type system and the simplest implementation. Moreover, there are lot's of courses, reference implementations, and reasonable extensions for a wide array of features (structural subtyping, qualified types, etc). There are even type-system libraries to make it easy to implement (like Inferno). When new programmer disc…

> If your types are not structurally too complicated

Load bearing hand waving.

Re: How to choose between Hindley-Milner and bidirectional typing

#32

Post by sheepscreek » Thu, Feb 19, 2026, 1:14 PM UTC

cardanome wrote: post #20

Does your language even need (complex) type inference? 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 rea…

I agree. HM or bidirectional typing works best when used optionally, allowing type hints only where needed.

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.

Re: How to choose between Hindley-Milner and bidirectional typing

#33

Post by thunderseethe » Thu, Feb 19, 2026, 1:33 PM UTC

StopDisinfo910 wrote: post #26

The real question is unification vs bidir more than HM vs bidir. 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. Anywa…

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

Re: How to choose between Hindley-Milner and bidirectional typing

#34

Post by thunderseethe » Thu, Feb 19, 2026, 1:36 PM UTC

cardanome wrote: post #20

Does your language even need (complex) type inference? 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 rea…

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

Re: How to choose between Hindley-Milner and bidirectional typing

#35

Post by StopDisinfo910 » Thu, Feb 19, 2026, 2:11 PM UTC

thunderseethe wrote: post #33

StopDisinfo910 wrote: post #26

The real question is unification vs bidir more than HM vs bidir. 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. Anywa…

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

Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others.

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.

Re: How to choose between Hindley-Milner and bidirectional typing

#36

Post by kccqzy » Thu, Feb 19, 2026, 2:22 PM UTC

nextaccountic wrote: post #19

kccqzy wrote: post #5

> What folks should actually be asking is “Does my language need generics?”. 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.

In this case do yourself a favor and use something like simple-sub https://github.com/LPTK/simple-sub https://www.reddit.com/r/ProgrammingLanguages/comments/hpi54... https://dl.acm.org/doi/10.1145/3409006

I have implemented simple-pub a few years ago in a toy project. And no, the type inference user experience is still way worse than what’s acceptable for a mainstream language.

Re: How to choose between Hindley-Milner and bidirectional typing

#37

Post by ruuda » Thu, Feb 19, 2026, 2:29 PM UTC

Drup wrote: post #23

cardanome wrote: post #20

Does your language even need (complex) type inference? 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 rea…

HM is not complex type inference. In fact, among all the approaches you cite, it leads to the simplest type system and the simplest implementation. Moreover, there are lot's of courses, reference implementations, and reasonable extensions for a wide array of features (structural subtyping, qualified types, etc). There are even type-system libraries to make it easy to implement (like Inferno). When new programmer disc…

It's not complex, in the sense that the rules are simple, but simple rules can still lead to complicated emergent behavior that is difficult for humans to understand, even if each of the 153 steps that the typechecker took to arrive at the result were easy to understand individually.

Re: How to choose between Hindley-Milner and bidirectional typing

#38

Post by kccqzy » Thu, Feb 19, 2026, 2:29 PM UTC

xmcqdpt2 wrote: post #29

Drup wrote: post #22

Earlier quoted context omitted.

I'm going to be contrarian: Yes, you should learn about type systems if you want to design a programming language, and decide in full conscience what you need. At the very least, it will give you a concrete idea of what safety means for a programming language. 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 mista…

Java also has covariant mutable arrays. I can't believe they created the whole language and didnt realize that covariant arrays are unsound? Or didn't care?

They didn’t care about preventing all unsoundness at type check time. As long as JVM can detect it and throw an exception, it’s good enough for Java.

Re: How to choose between Hindley-Milner and bidirectional typing

#39

Post by thunderseethe » Thu, Feb 19, 2026, 2:32 PM UTC

StopDisinfo910 wrote: post #35

thunderseethe wrote: post #33

Earlier quoted context omitted.

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

Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others. 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 a…

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

Re: How to choose between Hindley-Milner and bidirectional typing

#40

Post by tialaramex » Thu, Feb 19, 2026, 2:37 PM UTC

thechao wrote: post #31

Drup wrote: post #23

Earlier quoted context omitted.

HM is not complex type inference. In fact, among all the approaches you cite, it leads to the simplest type system and the simplest implementation. Moreover, there are lot's of courses, reference implementations, and reasonable extensions for a wide array of features (structural subtyping, qualified types, etc). There are even type-system libraries to make it easy to implement (like Inferno). When new programmer disc…

> If your types are not structurally too complicated Load bearing hand waving.

Very proportional to the hand waving in claim it was responding to that "in some cases" there might be a problem.