[Swizec]

> In general inferring which methods are valid on any given variable or expression is undecidable.

And yet, Hindley-Milner can do it. In general.

I've been working with dynamic and nontyped and weak typed and duck typed languages for over half of my life and you know what, it's getting ridiculous. They were never meant to support the team and project sizes we're forcing them into now.

[jules]

Hindley-Milner and other type systems do it by restricting the class of programs you are allowed to write. Essentially what they do is if they can't infer the type of a variable they terminate with an error. The class of programs that you are allowed to write is still reasonably big and Turing complete, but as research to make the type system more expressive shows, people want to go beyond that (higher kinds, GADTs, dependent types, polymorphic variants / structural records, subtyping, etc.). Type inference for a dynamically typed language can't terminate with an error if it can't infer the type, it has to be conservative in the other direction: if it can't infer the type of a variable it must assume that it can be anything.

[Swizec]

This was helpful! Now I have a bunch of new things to research and learn. Thanks!

[tel]

Of course you understand this, but for the benefit of the audience:

HM can do this because it dramatically restricts the allowable complexity of every single name in the program. This is rarely a problem, though, as typically you, as a programmer, only ever intend for names in the program to be so complex. The result is that HM simply ensures that your program is one which makes enough sense all of the time.

Which is sometimes painful for people when they first start.