Not Too Local type inference

Abstract

The type inference in statically typed, object-oriented languages is local because it needs to know the type of an object when a method is called or a property accessed on it, as multiple classes can implement the method/parameter with the same name. This is necessary to determine the type of the method/parameter. We introduce a language Inferable Featherweight Java (IFJ) which models statically typed, object-oriented programs with type information inferred partially. We define the type inference progression property for IFJ programs. If a program holds this property it has sufficient information inferred, so the type inference algorithm can determine all types of methods/parameters. We prove that type variables substituting phantom type parameters and type parameters used only on contravariant positions do not have to be inferred for a program to hold this property. Furthermore, we use this result to extend the reference type inference algorithm based on the programming language Kotlin, so it does not fail if unable to infer certain type variables based only on the local context. We consolidate those results as a feature proposal for the programming language Kotlin and integrate it partially into Kotlin's compiler. The new type inference algorithm allows certain type annotations to be left out in programs, most notably when working with algebraic data types.