A good bad idea: use a constraint solver to proove `when` exhaustiveness

1

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)
    )
  )
)

link to live running code

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.

3 Likes
2

Right now it seems like this feature is pretty predictable: if you want case coverage for the constructors of a union type it works, otherwise it doesn’t. If the feature were to grow general solving powers, but we still want some limit on compile times, it seems like the feature would be more useful but less predictable: sometimes you would add a branch and the compiler would give up, saying “solver timeout (200ms)”. Maybe on a faster computer it might work.

If the language/tools were to provide support for external verification, I wonder what that would look like? It seems like you’d want to have a pass where the compiler provided as much type information as it could, then a second pass whether the verifier looked at all the ill-typed or ill-formed expressions that remain, and then a pass that used that information to finalise the types.

3

You would need to find a solver that supported deterministically limited queries, i.e. not wall clock time limited but number-of-operations limited.