Kotlin has !! to convert a nullable type to a non-null type when the programmer is sure the type system is wrong and would prefer to have a runtime failure instead. This crops up a LOT especially when working with existing Java code.
Pretty ugly. The !! doesn’t really add much, it’s just type system noise.
If Kotlin automatically added !! wherever assignments or returns happened and it was needed to make the code compile, the type system would still carry nullability information and a runtime exception would be thrown at the earliest possible point. The downside is the programmer might not notice they auto-coerced away the nullability and lose a chance to write explicit handling code. IntelliJ could compensate by simply highlighting the code with a nice pastel shade to indicate possible NPE points.
Right now there are two ways to handle the !! infestation:
@NotNull annotation
Using external annotation
At some point you need to tell the compiler explicitly that this possible null value is actually safe. Swift programming language uses a single ! for this conversion.
Neither of those approaches solves the (quite common?) case of a method that returns an optional value, but the programmer knows that in fact it will never return null at that point. In the commit I linked to you can see this issue quite clearly, it does things like:
where the second element must exist because you just created it, but the type system itself can’t know that, so you have to override it. This is despite that the given function is only one or two lines long and the return type is clearly visible right next to the expression itself, so the !! does not add any code clarity that would otherwise be lacking.
How about a simple rule like this:
For single expression functions, nullability is automatically checked and casted away if the return type is not also nullable
The single expression function requirement would ensure that it can’t possibly hurt readability because the type is right next to the code anyway. On the other hand, perhaps such special exceptions would just be too confusing and not worth the prettier code?
Yes sure, but this probably gets us into general algebraic dependent types territory. GADTs are incredibly complicated and only show up in research FP languages from what I understand, so I doubt it's appropriate for Kotlin. A less ugly way to loosen the type system seems a better compromise for now.
There might be a few cases where it can be done more simply. If Kotlin has a way to mark functions as strongly pure in the manner of D, theoretically the compiler could actually execute the function at compile time, then use the output to discover that the accessor could never return null, but that’d slow down compilation a lot and I doubt it’s worth it.
It's not ready yet, so no sneak preview is possible.
On the “auto-cast proposal”: I think it largely defeats the purpose of the whole null-safety idea, beacuse you are essentailly proposing to have it the Java way.
The type system still carries the same information as before. If you see "val a: Foo" then you know a cannot be null, and that's useful information to have.
Additionally, the auto-cast means that nulls are discovered and turned into exceptions at the earliest possible time instead of propagating. Java programs use lots of checkNotNull() at the start of methods and constructors to try and fight this problem but Kotlin would not need it, because the act of calling a function with two non-nullable params with two nullable types would throw at that point even if the values weren’t used until much later.
Let’s look at it another way - what value does the programmer derive from seeing !! explicitly? He knows an NPE can be thrown at that point … but this is hardly ever useful as most programs do not try and catch or handle such errors. It could just as well be an IDE hint using colouring or a “show possible NPE points” hotkey.
Well, this is a plausible approach, very much like what Fantom language has (http://fantom.org/doc/docLang/TypeSystem.html, see "Implicit casts"). In Kotlin, we are more strict about typing: the type system is there to guarantee absense of errors unless the user explicitly requested the unsafe behavior.