Designing Kotlin Beyond Type Inference | Ross Tate

Ross Tate explains how Kotlin's next-generation typing algorithms can determine program safety more efficiently than traditional type-inference algorithms.

Recording brought to you by American Express. americanexpress.io/kotlin-jobs Kotlin programmers regularly elide uninformative types from their programs. This makes Kotlin programs faster to develop, easier to read, and less effort to maintain. It also means the Kotlin language needs to be designed so that its compilers can reliably accept programs without these typing hints. We think of this as type-inference, but—by definition—type-inference means determining these missing types can be filled in such that the program type-checks. But what if we can determine a program is safe without determining these missing types? What if we can do so even when it such types do not exist? And what if we can do so more efficiently than any type-inference algorithm can? In researching Kotlin's next-generation typing algorithms, we have discovered we can efficiently exceed the capabilities of type-inference and type-checking. We have developed a type-"outference" algorithm that efficiently decides "type-consistency", which all type-inferable/checkable programs satisfy (but not vice versa). While type-inference still has its place in user feedback and compilation, type-consistency is a much more flexible property, and type-outference offers clear guidelines on how to design features for efficient validation. In this talk, after introducing these concepts, we will provide a behind-the-scenes look into how they guide the design of various expected and hypothetical features for Kotlin, such as union types for errors, conditional inheritance for type-safe equality with value types, and implicit polymorphism for non-escaping references.