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:

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.

About Andrey Breslav

Andrey is the lead language designer working on Project Kotlin at JetBrains. He also works on making the Java language better, serving as a Java Community Process expert in a group for JSR-335 ("Project Lambda"), and occasionally speak at software conferences such as Devoxx or JavaOne.
This entry was posted in General, Language design and tagged . Bookmark the permalink.

16 Responses to Mixed-Site Variance in Kotlin

  1. Guangyu He says:

    This feature is very important, and I want to write an endorsement email to support it. However , I can’t find the EMail address of Ross Tate. Can you help me ?

  2. Anat says:

    Going over your paper, I think its basic assumption is flawed. The claim is that declaration-site variance cannot capture certain cases, such as wanting a read-only or write-only array along with variance.

    I give you a short Scala example:


    class ArraySource[+A](peer: Array[A]) { def apply(idx: Int): A = peer(idx) }
    class ArraySink[-A](peer: Array[A]) { def update(idx: Int, v: A) { peer(idx) = v }}

    So, I don’t see what the contribution of the paper is or what it tries to solve. I cannot make out a strong argument for use-site variance. Trying to get away with it by saying, well it might not be scientific but based on “industry experience”, doesn’t suffice.

    • Ross Tate says:

      Hello Anat,

      You bring up a good point, and one I feel is important to address, so thank you for mentioning it and giving me the opportunity to discuss it.

      I do not mean to claim that use-site variance can express things that declaration-site variance can’t. In fact, I mention in the paper that use-site variance can be encoded with declaration-site variance. However, you have to jump through some hoops to do so. Your counterexample is one such hoop. But a good language design will remove such hoops when possible; it will try to provide the means for programmers to concisely express common patterns. My point is that a read-only or write-only array or mutable list is one such common pattern that cannot be expressed with declaration-site variance without jumping through some hoops. Furthermore, those hoops can have unexpected consequences. They can break type-checking algorithms or slow them down. They can introduce inefficiencies at run time. They can change the semantics of programs in subtle ways. Sometimes they may work for certain cases but not all cases.

      Since you provide an example, let me use it to illustrate a few of these points. First, your system requires the programmer to explicitly cast from a general array to a read-only or write-only array, putting a burden on the programmer and essentially defeating the purpose of subtyping. Scala has implicits though, so lets put aside that issue (and the issue that implicits have all sort of algorithmic and semantic issues) and suppose that has been addressed. Then the next issue is that you have introduced a dynamic allocation where one was not present before, making performance slightly less efficient. Also, if ever this wrapper object is provided to someone as some interface, say Iterable, you’ve added another layer of dynamic dispatch with methods on the Iterable are called (and without use-site variance there is no way to extract the original object beforehand in order to avoid this overhead). Moving on, this new wrapper object has a different address than the original object, which will screw up address-sensitive algorithms/systems such as caches or anything using addresses to identify when two things are backed by the same state. Lastly, your trick would not work for all such situations, such as the following:
      class MutableSortedList[T <: Comparable[T]] {...}
      You might try to add the following covariant wrapper as you did with Array:
      class ReadableSortedList[+T <: Comparable[T]](MutableSortedList[T] peer) {...}
      However, Scala will reject this because Scala (unnecessarily) disallows a class’s covariant type parameters from appearing in constraints on that class’s type parameters non-covariantly; in this case it complains about the non-covariant usage of T in the upper bound Comparable[T]. You might think to drop that constraint, but then Scala (again unnecessarily) rejects the type MutableSortedList[T] of the constructor parameter “peer”, complaining that T is not a subtype of Comparable[T] as required by MutableSortedList.

      I hope that answers the concern you raised, Anat. The paper contributes a way to remove some common hoops. Furthermore, I went through a lot of effort to try to not add any new hoops. In particular, one awesome thing is that this is completely compatible with declaration-site variance. So, Anat, if you are not persuaded, you can choose to use only declaration-site variance in a language with mixed-site variance and everything will work exactly as if the language had only declaration-site variance – the feature will be completely invisible to you. You will have some difficulties interacting with libraries that do make use of use-site variance, such as many of the Java libraries, but I left that choice to you, which again I think is an important goal for language design.

      Thank you for taking the time to read the paper!
      Ross

      • Paul Phillips says:

        In case you are unaware, scala’s variance restrictions can be relaxed with an annotation.

        import scala.annotation.unchecked.{ uncheckedVariance => uV }
        trait Comparable[T <: Comparable[T]]
        trait Mutable[T <: Comparable[T]]
        trait ReadOnly[+T <: Comparable[T @uV]] extends Mutable[T @uV]

  3. Onne says:

    It make me wonder if type systems are worth it. I’ve put in production large systems in Java but also ocaml and scala, and sure the type systems helps while developing, but sometimes it is just a nuisance.

    Also I’ve put in production rather large systems, written in untyped languages, lately javascript. And in production, the problems that arise are very rarely problems a type system would have caught. Surely during development and testing you hit these enough, but they are always quick and simple to fix.

    I would pose that a type system is not strictly necessary, given the large body of production code out there making money, where types or not checked by any compiler. And with advances in VM/JIT designs, the types also are not necessary for performance, coupled with the fact that current machines are *really* fast. And just the business tradeoff, machine time/cost vs engineering time/cost.

    Now the ocaml type system is a lot less work then java’s. But explaining tricky code to my coworkers is never fun. Where usually the tricky part is only the type system. In javascript things would just fit naturally.

    My personal experience is that developing in a dynamic language is less work, getting from zero to production.

    So types are a tradeoff, some safety checks, at the cost of developer performance. Are these costs worth it? Or will languages like kotlin and ceylon (scala?) tip the scale by adding more convenience and more safety?

    But then discussions like above with Anat, they scare many developers away. And in javascript, all that discussion just dissolves to nothing, the code runs, or it doesn’t.

    • To my experience, the trade-off is the other way around. Types enable refactorings, code completion and other tooling support, which make developers a lot more productive.

    • Ross Tate says:

      Hi Onne,

      My opinion is that types have their place, but that place isn’t necessarily everywhere. You may be interested to know that I and many other researchers are investigating ways to mix typed and untyped systems. There are a lot of surprising challenges to getting this to work, such as having the typed code be able to execute efficiently and safely without worrying about the untyped code overstepping its bounds and screwing everything up. There are lots of applications of this, such as allowing programmers to write in mostly untyped code while also having the ability to type check core pieces that need, say, improved efficiency, better safety, or clearer documentation. Kotlin is particularly interested in the interoperability feature of this research, so there should be some cool new language features coming up along this line.

      As for the discussion with Anat, I think it shows that type systems are harder to design than you might expect. However, a good type system, even if it was hard to design, should be easy to use. That’s easier said than done though, so, as your experience suggests, there’s still plenty of work to be done!

      Thanks for discussing!
      Ross

  4. Ross, Andrey:

    I disagree about research rejecting industry evidence. POPL, and even more so PLDI, is very open to statements of the form “Experience in the field has shown that…”, especially when clear examples and metrics of usage frequency are available (as in your paper). What they are not amenable to is statements of the form “this is popular, therefore it is scientifically important”. Because such statements are false.

    The problems of mixing contra- and covariance in generics are well understood and acknowledged in the research community. The error message issues deriving from poor syntax choices are scientifically uninteresting. There’s good design there (and I like what you are trying to do), but no science. I suspect that your choice of IN and OUT for the relevant keywords will generate strong resistance. While I personally like the intuition you are reaching for, it’s an intuition grounded in side effects. The PL community is type biased, so using “super T” and “sub T” may go over better in that community. So, e.g., a use-site declaration Array meaning “I only want that part of Array that can be correctly be used under the assumption that all elements instances are of some supertype of Number”. If this is adopted, then Array should be understood to mean exactly type number. Hmm. You can rotate keywords here to accomodate common usage, but those are the three cases you need to cover: super, sub, exact. The only question is which one is the default in absence of explicit specification. That’s a syntactic matter that impacts error messages, but is irrelevant to the science.

    Aside from the initial discussion of why there is a problem to be solved, which is experiential, not hearsay, I see no hearsay in the paper. I think the call for industry endorsement is therefore irrelevant, and I also think it’s premature. I therefore think it will harm your chances of publication success while serving no purpose, and should be dropped.

    Jonathan Shapiro
    - the BitC Guy

    • Ross Tate says:

      Hi Jonathan,

      Thank you very much for your perspective. I agree that popularity does not make a solution good, and that is not my intent with this experiment. My understanding is that reviewers wanted the arguments for why the problem is important and why the solution is designed the way it is should be supported scientifically. It was not that the reviewers disagreed with the arguments, just that they felt such arguments should have scientific backing. Unfortunately this paper is centered around very human aspects of language design. This makes them very hard to study scientifically, as you need a sample set that is educated enough to have useful opinions/experiences and also unbiased enough to draw meaningful conclusions from, yet the education process itself introduces lots of bias. So, since the issue was justifying motivations and directions, not correctness of the solution, I figured I would try to find a way for industry to voice its assessment of these arguments (note that I say “endorsement” only means agreement with the arguments made, not necessarily with the solution I produced from those arguments). I am well aware this is a risky venture for myself and the paper (though the paper had already been rejected anyways), but I felt the side effect of broadening lines of communication with industry was worth the risk. It has been an interesting experience with some unexpected good consequences, but we’ll see if it does anything to help with future conference submissions.

      Thank you for your guidance!
      Ross

  5. David M. Lloyd says:

    I found this paper to be a great read, and at first reading at least the arguments seem very reasonable and valid to me. I did want to point something that jumped out at me on my first read though.

    First, the section 2.1 Types contains the line “Also, a language does not actually need a ⊤ or ⊥ type, and of course classes/interfaces can have an arbitrary number of type parameters, but we elide those details as they are not relevant to the intuitions, challenges, or algorithms.”

    I guess you do use the word “need” – and there are many things we don’t really need – but there are many uses for both top and bottom types. Of course we all know Object in Java which passes for a “top” type, and whose benefits (and drawbacks) are probably well-understood and well-documented at this point. However it is also worth noting that in many ways, the “null” value in Java behaves as if it were a reference value of a “bottom” type, and in fact this is a practically applicable and useful property in Java. Furthermore I contend that supporting other “bottom”-ish null-like reference values would have practical application, especially in concurrency code, where it is often useful to have “marker” values of various meaning. In Java we can often take advantage of erasure and use special Object instances, often cast “unsafely” to a type variable’s type in a data structure setting, for this type of purpose e.g. “missing but not null”, “pending deletion”, “end of queue/poison pill” etc.

    I have noticed a trend, especially in JVM languages for whatever reason, to shy away from the separated concept of primitives and references and objects and instead try to collapse them into one idea, somehow – a trend which I have always felt is a conceptual dead-end – but I think it’s important to note that top and bottom types, and even variant types in general, are properties of references, not of objects, even if the referential concept is hidden. By embracing the referential nature of objects, and expanding the world of references from just “good” object references and “bad” null references (my words, but I think this reflects the views of many Java users), I think there is a lot of power to be gained – and a nice cognitive resonance with respect to CPU architectures as well, which can often utilize “special” pointer values to implement these non-object reference values very efficiently.

  6. David M. Lloyd says:

    A comment on in/out versus other options. I have (in other contexts) been known to pine for the ability to use + and – to mean “super/extends”, but after reading your paper a couple times I now think that it would have been better if you could express bounds as bounds like this: Foo<Upper..Lower> or Foo<Upper:Lower>, using a blank to represent top or bottom: Foo<:Lower> or Foo<Upper:>.

    (Hope that all renders right…)

  7. claudiu says:

    dear, kotlin’ eers, not so many, but active. Is possible to tell when a stable version will be release, scala is killing me :(, at start was so fun and joy, but now, is .. jesus :(

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code class="" title="" data-url=""> <del datetime=""> <em> <i> <q cite=""> <strike> <strong> <pre class="" title="" data-url=""> <span class="" title="" data-url="">