[tomp]

You can count the number of type systems that are "logically OK" (the formal terms are sound (doesn't admit wrong programs, unlike e.g. Java), complete (can admit all correct programs (for some definition of "correct"), unlike e.g. Scala), decidable (always finishes)) on one hand. The rest amount to various amounts of hacks - common ones include specifying function parameter types to allow type inference to function, various escape hatches (like Object in Java and interface {} in Go), generics incorrect or limited to various degrees. Subtyping is tremendously hard. The specific hacks implemented in different programming languages are often implementation-specific (and arbitrary), and often result in weird interactions between different language features.

Basically, type systems == science (figuring out new things), programming languages = engineering (making new findings useful).

[TheAsprngHacker]

> You can count the number of type systems that are "logically OK" (the formal terms are sound (doesn't admit wrong programs, unlike e.g. Java), complete (can admit all correct programs (for some definition of "correct"), unlike e.g. Scala)... on one hand. The rest amount to various amounts of hacks

Huh? Rice's Theorem states that any static semantic analysis must either reject valid programs or accept invalid programs. This says nothing about whether a type system is rigorous or hacky.

> common ones include specifying function parameter types to allow type inference to function

It's true that type inference becomes undecidable without annotations for things like dependent types, and there's nothing hacky about that.

[ImprobableTruth]

Rice's theorem only aplies to turing complete programs, so if youre "weak enough" there's no problem being both sound and complete. I think it's easy to see why people would think of such systems as "nicer" (even though the others are of course still rigorous).

>It's true that type inference becomes undecidable without annotations for things like dependent types, and there's nothing hacky about that.

But it's not just for more advanced type systems, type inference is undecidable for basically any system more complex than HM typing. So in practice virtually all programming languages with type systems that go beyond the absolue basics can't fullfill the "promise" of type inference, which is that you don't have to explicitly annotate types. I think if you take into consideration that even relatively "good" type systems like Haskell's occasionally require you to annotate not just functions, but 'random' terms, you might see why some people might consider it "hacky".