Hey Guys,
It may or may not surprise you to know
val x = when {
true -> "testing!"
}
does not compile, because the when statement is not exhaustive, when, of course, it obviously is.
Rephrased, the compiler refuses to investigate anything other than sealed class hierarchies with respect to their exhasustiveness of a when statement. the compiler itself only considers 3 classes of when statements, those with an else
clause, those without an else
clause, and those on a sealed class hierarchy. The first is always non-exhaustive, the second is always exhaustive, the last is exhaustive iff every sealed class member exists as a clause.
I feel like its worth mentioning that this is probably the single most direct application of SAT/SMT solvers I have ever seen in compilers.
So lets make this a language feature request and merge it into kotlin! We can evolve it to make it increasingly general purpose, and then dump this problem of what is an exhaustive when expression onto a community that has a great deal of expertise proofing equations just like this. For example, it would be relatively trivial to transform
val x = when(someNullableInteger){
null -> A()
in Int.MIN_VALUE .. 0 -> B()
in 1 .. Int.MAX_VALUE -> C()
}
which effectively has the compiler asking the question
is the the universe of all possible
Int?
equal to {null
,MIN_VALUE .. 0
,1 .. MAX_VALUE
}?
which can be rephrased as
does there exist a value that is an
Int?
that is not in {null
,MIN_VALUE .. 0
,1 .. MAX_VALUE
}?
transformed into smt-lib2 expression:
(declare-const nullableInt Int)
(assert (! (= nullableInt [null])))
(assert
(!
(and
(>= nullableInt -2147483648)
(<= nullableInt 0)
)
)
)
(assert
(!
(and
(>= nullableInt 1)
(<= nullableInt 2147483647)
)
)
)
for which Z3 will in fairly quick time come back with UNSAT
, meaning it can generate a proof that there is no value outside of your when expressions, IE that your when statement is exhaustive.
So can we bolt this on to the kotlin compiler now?
The answer is almost certainly no. While SMT solvers will advertise that they work in the general case (and indeed, Z3 is used by pex in many very general cases), they have very little in terms of time-complexity guarantees. The Z3 solver effectively reserves the right to spin the CPU asking questions that it will never finish asking, in effect stalling the calling-compiler. So thats no good.
But this has me asking the question: what kinds of performance guarantees would the kotlin compiler team need to consider such an idea?
On the one end we have the go-lang guys who have deliberately structured their language such that its easy to parse, and then we have the scala guys who have a language riddled with complex ambiguity and sophisticated resolution rules but many more language features. What do you guys think kotlin should aim for?
I personally would really like more features around the exhaustive-when as is this is one of very few language options where you can explicitly introduce a compiler error when somebody makes a change that your code likely isnt prepared for, which is an enormously powerful tool, in my eyes.