Skip to content

Latest commit

 

History

History
190 lines (138 loc) · 12.8 KB

TypeProblems.md

File metadata and controls

190 lines (138 loc) · 12.8 KB

Сломанный сабтайпинг(KT-7296)

class Inv<T> {}
class A<T> {}
class B<T> extends A<A<T>> {}

java считает, что Inv<B<?>> подтип Inv<? extends A<A<?>>> но это не типобезопасно. Пример с CC: https://youtrack.jetbrains.com/issue/KT-7296#comment=27-1413390

При этом B не подтип A>

Почему так происходит. Дело в том, что на топ-левеле мы можем captured типы создавать, а вот на 2-м уровне и выше -- нет. Из-за этого в случае B<?> <:? A<A<?>> мы создаём exist Q.B<Q> <:? A<A<?>>. Далее это превращается в A<A<Q>> <:? A<A<?>> и обламывается, т.к. A<?> != A<Q>.

В случае Inv<B<?>> <:? Inv<? extends A<A<?>>> мы делаем иначе -- из-за ? extends мы должны проверить, что B<?> подтим A<A<?>>. При этом, мы не на топ-левеле, поэтому java считает, что тут нельзя применять capture conventions. И она радостно считает, что у B<?> подставленный супертип есть A<A<?>. Естественно что после этого A<A<?>> оказывается подтипом A<A<?>>. Тада.

Починить это можно так: сказать, что при проверки сабтайпинга можно всегда применять capture, даже в каких-то, казалось бы, не связанных с этим случаях. Аля Inv<in Number> <:? Inv<out Comparable<*>>. Да, capture надо делать только с левой частью выражения и только на топ-левеле.

Подумать: как это уживается с упрощением констрейнтов в констрейн системе?

Звёздочка и котлин (KT-11979)

https://jetbrains.slack.com/archives/kotlin-design/p1460667989000618

class Bar<T>(val t: T)
class Foo<F : Bar<F>>(val f: F)

val f: Foo<*> = TODO()

Если мы возьмём тип у выражения f.f, то он сейчас будет Bar<*>, но при этом там * имеет весьма специальную странную природу. Дело в том, что если мы посмотрим тип у f.f.t, то он тоже будет Bar<*>. Это значит, что звёздочка "помнит" про то, какой у нее супертип. Но при этом сабтайпинг это продалбывает и считает, что у него обычный такой тип Bar<*>.

Собственно можно получить CC. Пример тут: https://youtrack.jetbrains.com/issue/KT-11979

Починка: Foo<*> значит следующее: Foo<[]>, где когда у [] мы спросим, что же это за проэкция, он нам скажет out Bar<[]>, где если мы опять спросим, что же там за [] нам ответят out Bar<[]> и т.д. На самом деле, всё примерно так сейчас и происходит, но из-за того, что в компиляторе звёздочка параметризованная(у неё есть неявный супертип) то не корректно считать, что Bar<A> подтип Bar<*> для любого A.

Пусть есть декларация interface A<T : Number>. тогда согласно следующему параграфу тип A<out List<String>> корректный, а в компиляторе он сразу трансформируется в тип A<out List<String> & Number>

Type projections

Собственно вопрос. В каких случаях Foo<in|out Type> является корректной проекцией?

У javac-ка ограничения довольно странные -- там говорится, что мы, дескать, совсем фигню не должны писать, а именно что если декларация такая: Foo<T extends Number> то тип Foo<? extends String> не корректный, т.к. два класса в супертипах для ?. Там есть ещё всякие ограничения, но если после ? extends|super стоит какая-то типовая переменная, то многое не проверяется. И появляются вот такие вот примеры: https://www.facebook.com/ross.tate/posts/10102249566392775?pnref=story

Предлагается сделать так: чтобы проверить, корректно ли брать тип Bar<in A, out B, C> надо сделать следующее: взять типовые переменные X, Y, Z, подставить их в изначальную сигнатуру и добавить в систему ограничения что X подтип своих upper bound-ов, аналогично Y и Z. Затем, добавить ещё ограничения X >: A, Y <: B и Z = C ( если *-ка, то ничего не добавлять) и после этого проверить, что в системе нет противоречий. Грубо говоря, это означает, что никаких новых условий на внешние типы такой проекцией мы не добавили.

При этом, если у нас class Bar<T : A> а мы пишем Bar<out B> то если мы хотим заглянуть в мембер скоуп такого типа, то мы должны сделать следующее: создать Q такое, что Q <: A, Q <: B. после этого построить мемберов для Bar<Q>, а потом для них применить аппроксимацию.

Если аппроксимация обламывается, то мы всегда можем параметры вывести как Nothing, а return type как Any.

Печаль: Пусть class Bar<T : Number> тогда для Bar<in Int> нету развёрнутого представления в языке :(

Аппроксимация Росса.

http://www.cs.cornell.edu/~ross/publications/mixedsite/mixedsite-tate-fool13.pdf Собственно предлагается ей следовать. Там не описано, что делать в случае, когда captured переменные имеют среди своих собственных надтипах типы, в которых есть другие captured типы.

Разберёмся на примере:

exist A: ArrayList<B>, B . HashMap<A, B> 
<: exist A: ArrayList<B>, B . HashMap<A, out Any?>
<: exist A: ArrayList<B>, B . HashMap<out ArrayList<B>, out Any?>
<: exist A: ArrayList<B>, B . HashMap<out ArrayList<out Any?>, out Any?>
= HashMap<out ArrayList<*>, *>

В случае, когда у нас этот процесс не заканчивается(например exist F : Bar<F> . Foo<F>) предлагается в какой-то момент просто забивать и аппроксимировать к Any? и Nothing соответственно.

Вопрос: Возможно ли создать такой пример, в котором обрыв аппроксимации приводил бы к некорректному типу(см. прошлый параграф)

Intersection types and constraint system

Ну... всё плохо. В общем, в java верен инвариант, что intersection тип бывает только из proper типов, что очень хорошо. Они его представляют почти как captured тип, у которого есть несколько upper-bound-ов, и T может быть равен ему. Собственно, с incorporation-ом тоже нет проблем, т.к. если C <: A&B, то это тупо C <: A & C <: B. А если в другую сторону, то это ведёт себя так же, как C#1 : A, B и C#1 <: D.

И, кстати, инвариант скорее всего не верен, т.к. captured типы, пойду попробую пример написать.

Проблемы начинаются если T & Any <: String. Я не знаю, как из этого вывести, что T <: String?. Пример на котлине:

// FILE: 1.kt
package some

interface Inv<T>

interface B {
    fun <T> foo(f: Inv<T>): T
}

fun bar(b: String) {}

fun <T> id(t: T) = t

fun test(a: A, inv: Inv<String?>) {
    bar(a.foo(inv)) // Error:(14, 11) Kotlin: Type inference failed. Expected type mismatch: inferred type is String but String was expected
}

// FILE: A.java
package some;

import org.jetbrains.annotations.NotNull;

@kotlin.jvm.PurelyImplements("some.B")
public class A implements B {
    @Override
    @NotNull
    public <T> T foo(@NotNull Inv<T> f) {
        return null;
    }
}

Чисто поржать: пример для java, в котором от порядка деклараций зависит скомпилируется код или нет:

import java.util.List;
import java.util.function.Consumer;

public class TestO8 {
    interface X {
        void funX();
    }
    interface Y {
        void funY();
    }

    interface A extends Inv<X> {}
    interface B extends Inv<Y> {}

    interface Inv<T> {}

    public static <T> T intersectAB(Inv<? super T> i1, Inv<? super T> i2, Consumer<T> c) {
        return null;
    }

    public static <Q> Q getXorY(Inv<Q> i1) {
        return null;
    }

    public static void bar(Inv<A> ia, Inv<B> ib, Inv<List> il) {
        intersectAB(ib, ia,
                aAndB -> getXorY(aAndB).funX()
        );
    }
}

Если поменять местами декларации A и B, то нескомпилится.

Если подебажить, то окажется, что когда мы смотрим на A&B <: Inv<Q> то мы считаем, что это Inv<X> <: Inv<Q>

В общем, предлагаю попытаться сохранить инвариант о том, что пересекаем только proper типы. А случай с T &Any отдельно захакать, увы.

А вообще, если у нас Q это captured тип, и нам зачем-то понадобилось зафигачить Q <: SomeType, то возможны 2 случая:

  • SomeType это переменная системы. Тогда всё зашибись, так и оставляем, а ещё предлагается добавлять зависимость от переменных, которые есть в констрейнтах для Q на SomeType (кури JLS про порядок фиксации переменных)
  • Это какой-то там тип с какими-то там аргументами. Тогда мы должны найти supertype representative. Если Q : List<A>, List<B>, то мы увидим первый из них, ну в общем как в javac-е будет :(

Captured types

В общем, тут большой вопрос, в какой момент, собственно captur-ить. Пример в java: https://jetbrains.slack.com/archives/kotlin-design/p1461012425000028

Смысл в том, что мы не можем capturить из выражения с незаконченным инференцем, если оно возвращает T. В случае, если return тип просто Array, то тогда всё просто -- return тип преобразуем в Array<C#1>, C#1 <: T. О блин, не, не пройдёт в случае когда T должно вывестись из expected типа. Буэ. Надо будет покурить JLS ещё в этом месте.

Subtyping

Ха-ха, мы хорошо запретили вот это:

interface Inv<T>
interface A<X : Inv<Y>, out Y>

Т.к. мы это сделали, то проверять, что A<Inv, String> <: A<*, String> можно легко -- там где звёздочка, то игнорим, в остальных местах -- String == String.

Теперь остался только вопрос, что делать с проэкциями типа A<in ..., out ...> в супертипах. Ведь если мы разрешим много разных проэкций, то будет сложно понимать, что к чему.