ok so this: what if we introduced a SAT solver in...

# compiler

[groostav]

ok so this:

what if we introduced a SAT solver into the compiler?

Cons: your compilation times are terrible.
Pros: it would be really cool

[groostav]

note: a SAT solver would be able to infer that the three conditions A > B, and A < B and A == B cover all possible values, and thus you wouldnt need an else clause and the warning from intelliJ would be superfluous

[dmitriy.novozhilov]

Your cons is the reason why it won't be implemented never
Or, at least, until someone found the polynomial solution for SAT 🧌

[Dominaezzz]

There's a YouTrack for this somewhere

[hfhbd]

Yes, SAT is np hard, but I don’t think you will often use many variables. Take rust as example, it is able to solve some super set of these matching problems and the performance is still okay.

[Alejandro Serrano Mena]

you may want to check https://arrow-kt.io/ecosystem/analysis/quickstart/#running-the-analysis

[groostav]

so i've spent a fair bit of time with SMT solvers, I understand the performance implications, but as per @hfhbd's implication of the rust compiler, I wonder if there are some formalizims we can use on when statements to reduce the scope.

given that we've taken the step of making all when uses into expressions, removing then when statement, I think a logical step is to start pushing users away from else clauses in favor of better (SAT) proovably coverage statements.

In an ideal world, where size operators return a UInt, and you have such a sat solver, one could write something like

when(val it: UInt = list.size) {
  0 -> {}
  1, 2 -> {}
  in 3 .. 4 -> {}
  in 4 .. Int.MAX_VLAUE -> {}
}

This would give you a kind of pseudo sealed-class out of ints, which would be helpful if you're adding and changing sentinel values (ie, SPECIAL_SIZE -> ..

that said, if SpecialSize is computed or even soft-coded, as it is very likely to be, our solvers life becomes difficult.

So thinking aout it, it seems like a lot of work and a pretty huge chang efor not a lot of gain. 😕