Subtyping Reconstruction

[e2e4b6b7]

This issue is for discussion of the proposal to introduce Subtyping Reconstruction into the Kotlin language.
The full proposal text is available here: proposals/subtyping-reconstruction.md

The KEEP presents the Subtyping Reconstruction technique that introduces smart casts for generics.

Please, use this issue for the discussion on the substance of the proposal. For minor corrections to the text, please open comment directly in the PR: #410.

[kyay10]

Just clarifying, this would also be fine, right?

fun <T> evalWhen(e: Expr<T>): T = when (e) {
    is IntLit -> 42
}

[kyay10]

From "Can we fix these problems":

Fundamentally, this means we may need to add ways to encode recursive types (aka µ types) or some other ways to propagate such complex (e.g., recursive) constraints in the type system.

We leave the solutions to these problems for possible future work.

Would introducing Shape interfaces do the trick here? Just food for thought

[e2e4b6b7]

@kyay10,

Just clarifying, this would also be fine, right?

fun <T> evalWhen(e: Expr<T>): T = when (e) {
    is IntLit -> 42
}

Yes, it works in the same way as with any other Int-typed expression on the rhs. More precisely, in this case it is: T :> Int :> ILT and everything is fine.

Would introducing Shape interfaces do the trick here?

Yes, inferring only material interfaces will simplify everything, but there are some other issues. Therefore, we decided to address them separately to keep things manageable.

[RossTate]

I'm concerned about the approach to supporting this feature. The constraint resolution algorithm seems to have a lot of corner cases. For example, when resolving a constraint on a type variable, it goes through all the bounds on the type variable, but then it seems it can eventually generate a new bound on that same variable, which seems to create a non-terminating loop (or a loop that gets cut off arbitrarily). Even more worryingly, it seems hard to ensure the newly generated bounds conform to the invariants we can use to make typing efficient. For example, if every type variable has at most one upper bound, we can take advantage of this to keep subtyping and inference polynomial-time. But the proposed approach seems to enable adding arbitrary upper bounds to type variables, making these problems exponential-time. (I know some of these problems currently arise with smart casts, but there might be ways to fix this, whereas the proposed approach seems to make them unfixable.)

This feature seems to be expected to be used by advanced users with low frequency. Given that, would it make sense to look into decidable approaches that require a little more guidance/annotation from the user? For example, here's my stab at adapting the syntax for a known decidable approach:

when (variable of SuperClass<T>): WhenType {
   is SubClass<U> -> expr
   ...
}

Here we add this of SuperClass<T> clause, which declares type variables T to represent variable's type argument for SuperClass.
The WhenType then uses T to describe the type of the when expression, e.g. List<T>.
In the case is SubClass<U>, the U is yet another type variable, this time representing the value's type argument for SubClass (if it belongs to SubClass).
Suppose we have SubClass<X> : SuperClass<Set<X>>; then in this case the T in WhenType gets replaced by Set<U>, essentially incorporating the knowledge we gain about T from the fact that variable belongs to SubClass.
So, if WhenType were List<T>, then expr would need to have type List<Set<U>> assuming variable has type SubClass<U>.
We do this check for each case.
(When the U would not be used in a case, the user can elide them.)
Afterwards, if know that variable has type SuperClass<A>, and if WhenType were List<T>, then the when expression would have type List<A>.

In other words, the WhenType annotation tells us how to translate between the (possibly conflicting) information ensured by the type of variable and the invariants guaranteed by the various subclasses of SuperClass.
(I'm shoving details with variance and such under the rug.)

That's probably not very clear, so here is how it looks applied to various examples in the KEEP:

private val caller: Caller<M> = when (oldCaller of Caller<T>): Caller<T> {
    is CallerImpl.Method.BoundStatic -> { // Here T is substituted with ReflectMethod
        val receiverType = (descriptor.extensionReceiverParameter ?: descriptor.dispatchReceiverParameter)?.type
        if (receiverType != null && receiverType.needsMfvcFlattening()) {
            val unboxMethods = getMfvcUnboxMethods(receiverType.asSimpleType())!!
            val boundReceiverComponents = unboxMethods.map { it.invoke(oldCaller.boundReceiver) }.toTypedArray()
            CallerImpl.Method.BoundStaticMultiFieldValueClass(oldCaller.member, boundReceiverComponents)
        } else {
            oldCaller
        }
    }
    else -> oldCaller
}

sealed interface Expr<out T>
class IntLit(val i: Int) : Expr<Int>

fun <T> evalWhen(e: Expr<T>): T = when (e of Expr<X>): X {
    is IntLit -> e.i
}

sealed interface EqT<A, B> {
  class Evidence<X> : EqT<X, X>
}

class Data<S, D> {
  val value: D = ...
  fun coerceJsonToString(ev: EqT<D, JsonNode>): Data<S, String> =
    Data(when (ev of EqT<A,B>): (A) -> B { is Evidence -> { it } } (this.value))
}

// The above pattern of converting a value is pretty common, so here's a shorthand syntax for it:
class Data<S, D> {
  val value: D = ...
  fun coerceJsonToString(ev: EqT<D, JsonNode>): Data<S, String> =
    Data(when (ev of EqT<A,B>): (val x: A = this.value) -> B { is Evidence -> x })
}

sealed interface Chart<A> {
    fun draw(chartData: A)
}
class PieChart : Chart<PieData>
class XYChart : Chart<XYData>
fun modifyPieData(PieData): PieData {...}

fun <A> Chart<A>.customDraw(chartData: A): Unit =
  when (this of Chart<X>): (chartData: X) -> Unit {
    is PieChart -> {
      draw(modifyPieData(chartData))
    }
    else -> draw(chartData)
  }

interface A<in T, in V>
interface A1<in V> : A<Int, V>
interface A2<in T> : A<T, Int>

fun f(v: A1<*>): A2<Int> =
    when (v of A<T,V>): A2<T> {
        is A2 -> v
        else -> throw Exception()
    }
}

(I believe this is known as indexed pattern matching, albeit adapted to subtyping and inheritance rather than cases of an inductive data type.)

[kyay10]

@RossTate would this also basically allow existential types in subexpressions? What I mean is, Kotlin seems to have recently gained the ability to do something like:

data class Foo<T>(val list: MutableList<T>, val set: MutableSet<T>)
fun <T> bar(list: MutableList<T>, set: MutableSet<T>) { }
fun Any.baz() = when (this) {
  is Foo<*> -> bar(list, set)
  else -> {}
}

Where internally the type T of this@baz is the type argument to bar. Weirdly, the very similar

fun baz(foo: Any) = when (foo) {
  is Foo<*> -> bar(foo.list, foo.set)
  else -> {}
}

Does not compile. It sounds like your proposed idea would cover this usecase nicely too by allowing:

fun baz(foo: Any) = when (foo) {
  is Foo<T> -> bar<T>(foo.list, foo.set)
  else -> {}
}

Where T is a fresh type parameter (and perhaps even the type argument to bar would be unnecessary and inferred automatically)
Is that correct? Or would this be limited to only superclass-subclass situations?

[RossTate]

@kyay10 What you're touching upon is type capturing. There's a lot I could go into, but I think I'll just focus on the specific question you asked: yes, what I described would support "opening" the existential type. All of the following would type-check:

fun baz1(foo: Any) = when (foo of Any) {
  is Foo -> bar(foo.list, foo.set)
  else -> {}
}

and

fun baz2(foo: Foo<*>) = when (foo of Foo<T>) {
  is Foo -> bar(foo.list, foo.set)
}

and

fun baz3(foo: Foo<*>) = when (foo of Foo<T>) {
  is Foo<U> -> bar<U>(foo.list, foo.set)
}

They might be overkill for that particular example, but hopefully you can see how they can generalize to more complex examples.

[kyay10]

Apologies for the tangential conversation @RossTate. Would something like

fun baz4(foo: Any) = when (foo of Any) {
  is Foo<U> -> bar<U>(foo.list, foo.set)
  else -> {}
}

also be supported? Or would it have to instead be the mouthful of:

fun baz4(foo: Any) = when (foo) {
  is Foo<*> -> when(foo of Foo<T>) { is Foo -> bar<T>(foo.list, foo.set) }
  else -> {}
}

If the automatic approach in the KEEP cannot be made polynomial (maybe there's a way to modify the algorithm?), then I would like this more-explicit syntax, especially because it allows that explicit type-capturing. In fact, even if the automatic approach works, I like the explicit syntax anyways since it clarifies what's going on for the reader.

[RossTate]

Yes, your first (more concise) version of baz4 would work too.

[RossTate]

Here's a proof that subtyping reconstruction makes validation NP-Hard. In particular, given a graph, the following shows how to generate a program that is valid if and only if the graph is 3-colorable.

class Red {}
class Green {}
class Blue {}

class Vertex<V>() { public var vertex: V? = null }

sealed class GADT<out E> {}
class RedGreenGADT : GADT<Pair<Vertex<Red>,Vertex<Green>>> {}
class RedBlueGADT : GADT<Pair<Vertex<Red>,Vertex<Blue>>> {}
class GreenRedGADT : GADT<Pair<Vertex<Green>,Vertex<Red>>> {}
class GreenBlueGADT : GADT<Pair<Vertex<Green>,Vertex<Blue>>> {}
class BlueRedGADT : GADT<Pair<Vertex<Blue>,Vertex<Red>>> {}
class BlueGreenGADT : GADT<Pair<Vertex<Blue>,Vertex<Green>>> {}
// could have more cases...

fun <E> colorGraph(gadts: Array<GADT<E>>, addEdge: (E) -> Unit) {
    if (gadts[0] !is RedGreenGADT) return // After this, we know E :> Pair<Vertex<Red>,Vertex<Green>>
    if (gadts[1] !is RedBlueGADT) return // After this, we know E :> Pair<Vertex<Red>,Vertex<Blue>>
    if (gadts[2] !is GreenRedGADT) return // After this, we know E :> Pair<Vertex<Green>,Vertex<Red>>
    if (gadts[3] !is GreenBlueGADT) return // After this, we know E :> Pair<Vertex<Green>,Vertex<Blue>>
    if (gadts[4] !is BlueRedGADT) return // After this, we know E :> Pair<Vertex<Blue>,Vertex<Red>>
    if (gadts[5] !is BlueGreenGADT) return // After this, we know E :> Pair<Vertex<Blue>,Vertex<Green>>
    // Now I have 6 lower bounds on E
    // Note that I could also have achieved this with 6 different parameters of type GADT<E>, rather than a single array
    
    // For each vertex vi of the graph:
    val vi = Vertex() // introduces an unknown type denoting the color of vertex vi

    // For each edge vi -> vj of the graph:
    addEdge(Pair(vi, vj)) // due to the lower bounds on E, this is valid iff vi and vj are vertexes of different colors
}

[e2e4b6b7]

We had internal discussions about the NP-hardness introduced by subtyping reconstruction. We have an idea for overcoming these issues by tracking the consistency of the introduced bounds. For example, in the previous case, something like E :> Pair<Vertex<*>, Vertex<*>> will be inferred instead of six separate lower bounds. This idea requires further elaboration and verification, so it will be published in a few weeks.

[RossTate]

Documenting this proof of undecidability for a subset of the features in consideration as they are currently written (which is not to say they cannot be adapted), which I came up with by adapting an idea from Garrigue and Le Normand's GADTs and Exhaustiveness: Looking for the Impossible.

sealed class Symbol {}
class Symbol_blank: Symbol() {}
// For each symbol s:
class Symbol_s: Symbol() {}

sealed class Tape {}
class Nil: Tape() {}
class Cons<out Head: Symbol, out Tail: Tape>: Tape() {}

class State {}
// For each state s_i:
class State_i: State() {}

interface StepsTo<out Configuration> {
    fun next(): Configuration
}

sealed class Configuration<out Current: State, out Head: Symbol, out Left: Tape, out Right: Tape> {}
// For each "state s_i moves left and transitions to s_j when head is Input, replacing it with Output":
class Transition_i_j_Input<out Left: Tape, out Next: Symbol, out Right: Tape>
        : Configuration<State_i, Input, Cons<Next, Left>, Right>(),
          StepsTo<Configuration<State_j, Next, Left, Cons<Output, Right>>
// plus, in the case that Input is blank:
class Transition_i_j_nil<out Right: Tape>
        : Configuration<State_i, Symbol_blank, Nil, Right>(),
          StepsTo<Configuration<State_j, Symbol_blank, Nil, Cons<Output, Right>>
// For each "state s_i moves right and transitions to s_j when head is Input, replacing it with Output":
class Transition_i_j_Input<out Left: Tape, out Next: Symbol, out Right: Tape>
        : Configuration<State_i, Input, Left, Cons<Next,Right>>(),
          StepsTo<Configuration<State_j, Next, Cons<Output, Left>, Right>
// plus, in the case that Input is blank:
class Transition_i_j_nil<out Left: Tape>
        : Configuration<State_i, Symbol_blank, Left, Nil>(),
          StepsTo<Configuration<State_j, Symbol_blank, Cons<Output, Left>, Nil>
// For each "state s_i halts when head is Input":
class Halt_i<out Left: Tape, out Right: Tape> : Configuration<State_i, Input, Left, Right>()

// Suppose s_0 is the initial state
// The following is valid if and only if the Turing machine does not terminate
fun terminates(val initial: Configuration<State_0, Symbol_blank, Nil, Nil>) {
    var configuration = initial
    when (configuration) {
        is StepsTo -> configuration = configuration.next()
    }
}

In particular, Configuration does not itself implement StepsTo. However, for given "constant" type arguments Current, Head, Left, and Right, there is necessarily a single subclass of Configuration<Current,Head,Left,Right> that does implement StepsTo if there is a corresponding transition in the Turing machine. In which case, it has a next() method, the return-type of which is the configuration the Turing machine would step to. So the when is exhaustive if and only if the Turing machine does not terminate on the empty input.

Note that the hierarchy I used is not recursive.