Live data from Hacker News

How to choose between Hindley-Milner and bidirectional typing

thunderseethe.dev

21–30 of 50 posts

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

#21

If your type system is HM, consider a compositional type system instead, for much better explainability of type derivations and type errors: https://unsafePerform.IO/projects/talks/2016-06-compty/CompT...

that is the best use of non canonical domain name capitalization I've ever seen.

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

#22

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

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 mistake, has been done by badly designed type systems from the Java/C/C++ family.

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

#23

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

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

#24

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…

Type inference saves typing on the keyboard.

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.

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

#25
post #12

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

Probably not. Most popular programming languages have messy - unsound and/or undecidable - type systems e.g. C++, C#, TypeScript, Java,.. ..because that is more practical.

You suggest that the programming language developers made a conscious choice to implement "messy" type systems. That's not at all how it came about. These messy type systems are generally a result of trying to work with earlier language design mistakes. Typescript is an obvious example. The type system was designed to able to type a reasonable subset of the mess of existing Javascript. There is no need to make the same mistakes in a new language.

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

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

Anyway, here is my non answer: it's a trade off.

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

#27

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…

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

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!

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

#28

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…

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

If you have generics and want type annotations to type check at compile time, you are going to need unification,

let l: List = 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 = List(dog: Animal, cat: Animal)

but that doesn't seem particularly ergonomic.

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

#29
post #22

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

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?

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

#30
post #24

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…

Type inference saves typing on the keyboard. 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.

I don't think saving a few keyboard strokes is a worthwhile design goal for most languages. You have to keep the types in your head anyway so it just increases the mental burden when reading the code.

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.

Post reply on HN