Shouldn't each of these pre-condition calls imply ...

# getting-started

[Vampire]

Shouldn't each of these pre-condition calls imply that foo is non-null?
So why is the second foo call not working?

fun foo(foo: Any) = null
val foo: String? = null
foo(foo)
check(foo != null)
require(foo != null)
assert(foo != null)
foo(foo)

[Youssef Shoaib [MOD]]

Working for me 🤷🏼 (playground)

[Vampire]

Hm, yeah, in a normal Kotlin file it works, thx.

In a Gradle build script it does not.

[Huib Donkers]

Possibly unrelated to your problem, but I don't think the assert implies foo is not null. Assertions may be disabled when compiling, so we can't rely on the condition being true after the assert statement.

[Vampire]

Yes you are right, and I was about to submit a bug about that.

I see it just like a contract.
With

fun <T> T?.markAsNonNull() {
    contract {
        returns() implies (this@markAsNonNull != null)
    }
}

I can tell the compiler that I know better than him (for example due to wrong nullability annotations in Java).

With assert(...) I'd have expected the same, so that I can just write

fun foo(foo: Any) = null
val foo: String? = null
assert(foo != null)
foo(foo)

instead of

fun foo(foo: Any) = null
val foo: String? = null
foo.markAsNonNull()
foo(foo)

Of course this would fail when assertions get enabled as it actually is null and the receiver is the actual problem.
But in other cases it would work and should just have the same contract check and require have imho.

[Vampire]

Hm, already rejected, sad. 😞
https://youtrack.jetbrains.com/issue/KT-39315

[CLOVIS]

In Kotlin, we prefer that the compiler tells us something is safe when it knows it's safe, not when it infers the user says it may be safe. It's a big difference with e.g. TypeScript. Since without -ea there won't be any check, the compiler will not let you write code that assumes that check-that's-not-there would've passed.

[CLOVIS]

(said otherwise: don't use assert() for critical things)

[Youssef Shoaib [MOD]]

You can also easily introduce a strongAssert function that has such contract

[CLOVIS]

^ if you're going to do this, I'd name it assume

[Vampire]

Of course an own function with contract can be done like the markAsNonNull I showed above, that's not the point.

The sense of assert is, so that you can run tests with -ea and have the invariants checked, while at production time you can spare the time for those assertions by not enabling them.

But the actual assertions done by the assert should usually still hold and so imho the compiler should take them into account.
That they are true whether you enable or disable assertions is the whole point of them.

[CLOVIS]

Well, it's more "I hope it's true but I don't want to spend the time to actually check". The stdlib & compiler should provide code that's correct, it shouldn't rely on hope.

[CLOVIS]

It's the same reason !! does check, instead of just relying on the platform to throw an exception sometimes later

[CLOVIS]

I'm curious though, in which situation is a null-check so expensive that you'd want to remove it in production? The compiler already adds null checks at the start of every public function, they're not supposed to be expensive

[Vampire]

Well, it's more "I hope it's true but I don't want to spend the time to actually check".

No, it's more "I tested all possible edge cases in my tests and know that the condition is always true, so I don't want to spend the actual time for the check at production time".

With disabled assertions, this is exactly like a Kotlin contract.
The contract can say that this is non-null when the method call returns.
The compiler trusts your statement even if you later return null which is perfectly valid even if in most cases non-sense.

in which situation is a null-check so expensive that you'd want to remove it in production

Nowhere.
I was hunting a work-around for calling an ill-annotated Java method where Kotlin thought it it non-null while it is nullable.
So foo actually is null but I want Kotlin to think it is not so that the call is made.
Of course as I said the contract variant here is more appropriate as it works with both, enabled and disabled assertions.
But for the sake of this argument, just assume the null check is extremely expensive to do.

[loke]

@Vampire did you measure the impact of such a check? Even in my time-critical JVM code, I keep the checks, because the performance difference is barely measurable.

[Vampire]

What do you mean with "such a check"?

[Vampire]

I do not have checks that I don't want to do at production time.
But that is the sense of assert and thus assert should have the same contract as require and check.
I just tried to abuse assert as a work-around for a nullability bug.
But there are definitely checks that you don't want to do at production time, or the assert feature would be pointless and not exist.
The point is, that the compiler should still follow that contract whether the assertions are actually enabled or disabled.