[jfoutz]

Far and away the most obvious is null checking. It's not a big deal in a thousand line program, but as things grow, the need to always remember to check for null becomes a real problem.

Related to null, you only get one null. the classic assoc problem. if i lookup a key in a hash, does the hash have the key, or is they value of the key null? Optional/Maybe is just wonderful for this case.

Semantic meaning of common types.

    update(String name, String email, String address, ...)

vs

    update(Name name, Email email, Address address, ...)

Strings get overloaded for lots of uses, and it's so easy to swap the order when you have multiple arguments.

Status codes, stuff like Email vs VerifiedEmail. Encoding those random flags in types makes it so much easier to enforce rules.

Yes, they are all "easy", but we've all lost hours or days to those problems. The sooner we can stop worrying about bonehead, forgot to check for null errors, the sooner we can concentrate on real problems. They're trivial problems, but we waste a big fraction of our lives dealing with them. Just taking those issues off the table makes it possible for average programmers to find bugs in timsort. The cognitive load of these dozens of details detracts from average programmers (like me) ability to actually detect the hard cases.

Typing isn't a panacea, but it is a help. It's akin to a socket driver vs a wrench. sockets abstract away the need to remove rotate and refit the wrench for every stinking quarter turn. You can do it with a wrench, but it takes so much longer.

There are no silver bullets. but there are regular bullets, and a good type system is one of them.

[pron]

You don't need a rich type system for null safety. Something like what Kotlin offers[1] is more than enough (in fact, I think it's better than what languages with far richer type systems offer).

My point isn't that types are not helpful -- they are extremely helpful. My point it that on the continuum between no types and "types try to prove everything", there is a point that is the most useful, and that point is probably far from either extreme (I don't know if it's equally far from both, but I think it's pretty far from both).

[1]: http://kotlinlang.org/docs/reference/null-safety.html

[jfoutz]

I guess, it's hard to get a handle on the rare cases, because they are rare, each appears unique. Structurally eliminating the common problems frees up a lot of mental power to face the next most common problem.

I think, I'd rather have a type system that's too powerful and sometimes misapplied than have the "easy" but common problems i listed above. It makes the next level of error accessible to mere mortals.

I think you have a great deal of insight, but i don't think computer science is remotely close to being able to say, oh a type system only needs X power, beyond that we use this other tool.

[pron]

> i don't think computer science is remotely close to being able to say, oh a type system only needs X power, beyond that we use this other tool.

That's because that's not a problem for computer scientists to solve but for language designers. Programming language design is 5% theory and 100% psychology. The question of what's useful cannot be answered by math, but by psychology (well, it's determined by psychology, but could be answered with "clinical research").

[sold]

> in fact, I think it's better than what languages with far richer type systems offer

Can you explain why? I don't know Kotlin, but from this page it seems to divide types into nullable and non-nullable (correct me if I'm wrong). Is it possible to have a type "T??" that has three possibilities - "null", "wrapped null" and "T"? If not, this approach will not help in the assoc problem mentioned by the parent poster.

[pron]

The "assoc problem" is completely separate from null safety (it also demands a solution in a language without null).

Kotlin's handling of null safety is especially nice because of Kotlin's guarded casts. I.e. if you have a variable x of type A and B <: A, then within any block where the value of x is known to be of type B, the variable x can be treated as if it's of type B. So, because A <: A?, if you have x:A? and any test of the kind (x != null) -- it can be in an if, a subexpression of if, a while, a when -- then x can be treated as non-nullable. This, combined with handling nulls from Java[2] and how all this interplays with method and property access and the other operators make up a particularly nice way of handling nulls.

[2]: http://kotlinlang.org/docs/reference/java-interop.html