Comment by wyager | Hacker News Reader

Comment by wyager | Hacker News Reader

> The language is very opinionated about type safety... For example, the fact that a variable of type X might also be nil means you must declare that variable to hold an "optional" value... The extreme nature of the type system in swift

Oh boy, if he thinks that's extreme...

> Why am I wasting time satisfying the type constraints of Java when my unit tests are already checking everything?

Oh really? Are the unit tests testing every single 2^64 possible values of an Int? Are they testing for the existence of null everywhere you have a pointer? Strong types aren't just a little bit more info about something; they're a precise refinement of the nature of all values in a program.

While very few type systems can test everything you can test with unit tests, a decent type system and good semantics can cover all causes of crash failures and many causes of logic errors. Seriously, folks; writing programs that crash is more or less optional these days. Writing correct programs is still hard, but you can make it a lot easier on yourself.

> Are the unit tests testing every single 2^64 possible values of an Int?

Hmm...your usual type checker is checking 0 possible values of an int. It is checking just the type. And of course if you are checking a value in a test, you ar coincidentally also checking its type.

That's not to say that types can't be useful (for example they have been shown to be quite useful as machine-checked documentation for getting around unfamiliar codebases), but please let's not oversell...

The compiler can use the known bounds of a type to perform correctness checks or optimizations. It might not be testing every possible value of an int explicitly, but the compiler certainly uses the range of an int to make lots of decisions and produce warnings/errors.

In fact, it checks every predicate codified by the type system. The question is how powerful your type system is, because this determines what predicates you can (conveniently) test.

Well-designed strongly typed languages naturally check some useful predicates (existence, the exact structure of the value, etc.). These alone are sufficient to eliminate null pointers, non-total functions, and most other failure modes that plague languages like C++ or Python.

Stepping it up a notch, you can use things like GADTs and kind promotion to check much more advanced predicates (like that a vector must be non-empty or even length).

With refinement types a la liquid Haskell, I can statically guarantee that e.g. my function only returns lists of even length or only returns even numbers, without even having to put this information in the type of the returned value.

With full-blown dependent types a la Coq/Idris/Agda, you can encode pretty much whatever property you want into types. For example, Idris has `verifiedMonoid` which statically guarantees that an operation is associative and has an identity. See https://github.com/idris-lang/Idris-dev/blob/master/libs/con...

Reply on news.ycombinator.com