Kotlin's type system is unsound, too, albeit for a...

# random

[elizarov]

Kotlin's type system is unsound, too, albeit for a host of other reasons. This is not be treated as a problem, thought. Static type system is just a kind of static code analysis tool and all practical approaches to statical analysis of programs are unsound for good reasons: http://manu.sridharan.net/files/cacm15.pdf

[eladkay]

This is a long shot, but can anyone shed some light on what makes Kotlin's type system unsound? Kotlin should be resistant to Java's unsoundness proof from 2016

[Sam]

My go-to source for this stuff is normally https://counterexamples.org/

[hho]

I probably don't understand it right, but isn't !! already enough to break soundness? It makes stuff compile which normally shouldn't…

[eladkay]

It is a great resource indeed! I already gave it a look over and it appears that the only thing there that's relevant to Kotlin is this one about variance checking. I saw the YouTrack issue and it really appears more like a compiler bug: this shouldn't compile because listOf(1, 2).addAnything should have E = int, so it should be illegal to pass a string as a param. And this is done in static time so type erasure shouldn't be an issue.

[eladkay]

About !!, I guess that counts as much as "1 as String" counts. !! is an explicit cast which may fail, which is what we want. The problem is if !! converted the type T? of its operand to T in an unchecked way, allowing it to crash later

[eladkay]

A different way of thinking about it: !! is an operator from T? to T, in this sense, null!! operates legally as expected: it throws a type error

[hho]

OK. Platform types (from Java interop) can be used without said operator and blow up unchecked… Do those count?

// JAVA
class Demo {
    static String provideNull() {
        return null;
    }
}

// Kotlin
fun main() {
    println(Demo.provideNull().length)
}

[eladkay]

Hmm. Not really, I think. The type of Demo.provideNull() is not String but String! , and there's an implicit cast there to String before accessing `String`'s length property

[robstoll]

the compiler doesn't catch all cases when it comes to reified types and type erasure. You might end up with runtime errors where the compiler was all happy. See e.g. https://youtrack.jetbrains.com/issue/KT-27846/forbid-function-types-as-substitute-of-reified-types

[eladkay]

Is that a language design issue or a compiler bug? I guess it may be underspecified in the standard?

[Jason5lee]

The most memorable one for me is this: [Type-safety breach when 'is' check ignores variance incompatibility](https://youtrack.jetbrains.com/issue/KT-7972/Type-safety-breach-when-is-check-ignores-variance-incompatibility), which I have participated.

[eladkay]

I never understood that one, why isn't there a mismatch between the receiver's E and the param's?

[Roukanken]

@eladkay as mentioned in the counterexamples, the culprit is variance & type erasure.
MutableList extends List, which would lead one to assume that MutableList is subtype of List (and therefore check List<E> is MutableList<E> is safe, regardless of what is E, or where it comes from), but this isn't actually true from type theory standpoint.

To give concrete examples, take two concrete types, of which one is supertype of other - such as Any and Int, and draw a graph of types when you apply them to both list types. You get something like this, where A -> B means "A is supertype of B". Supertype relation can be looked upon as "A less concrete type than B", meaning that whatever you can do with A, you need to be able to do with B.

But from the graph drawn, there is one arrow missing for this to be true: MutableList<Any> is not supertype of MutableList<Int>, but over in the world of Lists this is true.

This causes the issue with the linked code - if you infer E to be Any, the code typechecks and is looks completely correct - element is String, so it's Any, this is MutableList<Int> so it's List<Any>, and MutableList<Any> is subclass of List<Any> so it makes sense that you can ask the is MutableList<Any> - but that question wouldn't be allowed if you still thought that this is MutableList<Int>. You somehow gained ability to do a new possible operation on it, via upcasting it... (And for completness, you can definitely store element: Any in MutableList<Any> )

TL;DR: List is weird, and both of these statements are true:
• For any given & concrete E , List<E> is supertype of MutableList<E>
• List is not supertype of MutableList

[eladkay]

This is intriguing! I'll have to let the implications of this sink in. Thank you so so much for the detailed response! @Roukanken