[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