4 ms·

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

> 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 7y ago
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".