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...
How to choose between Hindley-Milner and bidirectional typing
21–30 of 50 posts
Re: How to choose between Hindley-Milner and bidirectional typing
#22I 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?
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
#23Does 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…
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
#24Does 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…
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
#25I 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.
Re: How to choose between Hindley-Milner and bidirectional typing
#26Unification 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
#27Does 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…
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
#28Does 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…
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
#29I 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…
Re: How to choose between Hindley-Milner and bidirectional typing
#30Does 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.
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.