Kotlin
A concise multiplatform language developed by JetBrains
Mixed-Site Variance in Kotlin
Type systems… We all know they are cool. In a static language, like Kotlin, the type system is the one responsible for early detection of errors. Many tools (e.g. an IDE with its refactoring abilities) also rely on the type system.
We also know that type systems are hard: many computer scientists built their entire careers studying type systems. Yet we know rather little about type systems of main-stream languages.
For example, take a simple question: “We have two Java types, say, A and B; can I assign a value of type A to a variable of type B?” (In other words, “Is A a subtype of B?”) For some languages (e.g. C#) we know that there’s an algorithm that takes A and B, thinks for some time, then terminates and gives a correct answer: “Yes” or “No”. In other words, the subtyping problem is decidable for C#. For some other languages we know that there can be no such algorithm: whatever compiler you write, there will be a pair of types A and B on which it either gives a wrong answer, never terminates or throws an exception (which can be viewed as a wrong answer too). In other words, subtyping is undecidable for Scala (in fact, Scala’s type system is Turing-complete, i.e. you can make Scala’s type checker perform any computation, including an infinite loop).
What about Java? We don’t know (see this paper, for example). Some people suspect that subtyping is undecidable for Java, but this has not been proved to this day. Is this a practical question? Oh, yes it is. Some people want to add reified generics to Java, which means that foo instanceof Bar would be checking whether the run-time type of foo is a subtype of Bar. And if there’s no algorithm that can decide that, we are in trouble: instanceof will hang sometimes.
That’s why it’s important to study type systems of main-stream languages. And it’s a pity that so few researchers do.
That’s why it’s important to design your type systems carefully, too. So we collaborate with Ross Tate, an Assistant Professor at Cornell University, who is an expert in this field. Ross helps us figure out tricky bits of the type system, avoid nasty corner cases and keep it clean altogether. Recently he wrote an article about generics, including generics in Kotlin. It is very approachable and well-written, so I totally recommend it:
- Mixed-Site Variance by Ross Tate
You’ll find a “Call for Industry Endorsement” on the article page. It’s an important thing: although this kind of research is very important (as I explained above), the academic community isn’t really used to it, so we need to coordinate a little to help them realize that this kind of contribution is a good one. To quote that page:
Why should you bother? I (and many others) would like to help solve your problems. The challenge we face is that many of your problems are hard to discuss scientifically. Indeed, industry tends to improve by reflecting on experiences, at least when it comes to programming-language development. Unfortunately, we academics need to publish in scientific conferences and journals, and personal experience is not a scientific process. Our reviewers may very well like what we have to say, but they may not be comfortable accepting a paper founded on heresay into a scientific venue. Indeed, after reading positive reviews and then being rejected, through side channels I was informed such concerns were this paper’s downfall, and I was encouraged to try unconventional avenues. So, this is an experiment to enable industry to encourage research directions they would like explored despite the difficulty in scientifically backing claims. In other words, this is an attempt to make industry experience admissible as evidence in academic settings, just like they are in industry settings.
Ross (and I) will appreciate an endorsement email from you.
Thanks.
P.S. In the picture above you see Richard Feynman, a Nobel Prize winning physicist. He did not care about type systems, but he was a really interesting man, probably the most practical theoretician, and contributed to Computer Science by inventing quantum computers.
Subscribe to Kotlin Blog updates
