Compile Time Union Types: A Small Step forward towards Denotable Union Types

Language Design
1

The proposal about union types was not put forward by me first, see KT-13108. Here we only disscuss about Compile Time Union Types.
Currently, the type of when/if expression is the common super type(s) of each case. For example, the local varibale x in the following code was infered as Comparable<*> & java.io.Serializable.

var b = false

fun main() {
    val x = if (b) {
        1L
    } else {
        "OK"
    }
}

However, for exhaustiveness checks in when expressions, intersection types often encounter the following error. A NO_ELSE_IN_WHEN will be reported in the following code:

val y = when(x) { // error: NO_ELSE_IN_WHEN
    is Long -> "Fail"
    is String -> x
}

If we can infer the type of x as Long | String, the exhaustiveness check in the when expression becomes easier and more straightforward. Furthermore, we can also say that the following when expression is exhaustive.

val z = when(x) {
    is Number -> "Fail"
    is CharSequence -> x.toString()
}

That’s bacause the union type Long | String is the subtype of Number | CharSequence.
As for call resolution and codegen, we use the intersection types or a single common super as before. I believe union types will not have compatibility issues in the call resolution system.
I have created a draft PR (Support for non-denotable union types by XYZboom · Pull Request #5436 · JetBrains/kotlin · GitHub), an implemented simple prototype in here.

interface I1
interface I2

class A: I1, I2 {
    fun func(): String = "A"
}

class B: I1, I2 {
    fun func(): Int = 123
}

var b = true

fun main() {
    val aOrB = if (b) A() else B()
    val r = aOrB.func() // UNRESOLVED_REFERENCE because we do not use A | B in call resolution now
}

Further more, we may want more in call resolution. We may want this:

val r /*String | Int*/ = aOrB.func()

Resolve for aOrB::func may need redesign of the call resolution system. So in my opion, the previous solution is much better.
I hope this makes the idea clear. Thanks in advance for any reactions.

1 Like