It may be stupid/newbie question, but can I use co...

# compiler

[holgerbrandl]

It may be stupid/newbie question, but can I use contracts to check if method arguments are < 0?

fun foo(param:Int) {
// old school, but could we use a contract here to get compiler error at callsite for foo(-1) instead?
require(param >1)

// do something great
println(param)
}

[dmitriy.novozhilov]

No you can't

[holgerbrandl]

Would be cool though. 🙂

[holgerbrandl]

Could I achieve this with annotations?

[dmitriy.novozhilov]

IMO this feature has very limited use-cases
I heard that folks from #arrow-meta made something like this with their type proofs
cc @raulraja

[holgerbrandl]

Is it really that limited? IMHO all arguments checks `require(something)`that are typically just error at runtime could be handled at compile time (that is: could be flagged as red in the IDE).

[dmitriy.novozhilov]

Usually programmers don't call foo(-1) but call something like

val x = receiveDataFromSomewhere()
foo(x)

And in such situations simple contracts like foo requires that x > 0 won't work. To handle this you also need some function that provides information that some value is really > 0, which may add a lot of verbosity (imagine that you always need to check that index >= 0 before calling list[index])

I can agree that it can be useful in some situations, but currently it's not in our priorities.

[holgerbrandl]

I see, indeed with receivers, it would result in very deep code introspection. Thanks the nice explanation @dmitriy.novozhilov

[dmitriy.novozhilov]

BTW currently one of our interns works on prototype of such system to research how it may be implemented in compiler, will it heavily decrease compilation performance or not, how user code will looks with such contracts. And if this work will be successful than we may reconsider our plans about this feature
But this prototype is far away from finish

[raulraja]

We plan on implementing refined types more in depth in Arrow Meta once FIR and the compiler api is stable and supported by the IDEA Kotlin plugin. In the version we are prototyping type refinements are powered by a symbolic execution engine that can add complex constrains to data flow. If the compiler api provides a means to extend contracts we will use contracts and their declarations otherwise a means to annotate expressions. The current version we have is less powerful and uses compiler constants and the compiler std lib classpath deps to evaluate expressions at compile time but it’s quite slow and limited.

[holgerbrandl]

So cool, thanks for the updates @dmitriy.novozhilov & @raulraja

[elizarov]

The better way to write it (now) is this:

inline class PositiveInt(val value: Int) {
    init { require(value > 0) }
}

// Now, you can be 100% sure!
fun foo(param: PositiveInt)

[elizarov]

TLDR Contracts are not there to replace types. They are there to specify complex connections between params/returns that are not expressible via the type system.