[cardanome]

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

[Drup]

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

[ruuda]

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.

[ux266478]

It's not any different than having 153 steps in any other computational sense. Even limiting ourselves to elementary arithmetic, horrendous opaqueness arises with 153 operations spanning the whole set. Are we going to pretend like arithmetic is a systemically problematic because of this? Any non-trivial formal construct is potentially dangerous.

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.

[thechao]

> If your types are not structurally too complicated

Load bearing hand waving.

[tialaramex]

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

[xmcqdpt2]

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

[sheepscreek]

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.

[thunderseethe]

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

[somewhereoutth]

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

[pjc50]

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.

[cardanome]

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.

[ndriscoll]

> You have to keep the types in your head anyway so it just increases the mental burden when reading the code.

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