Higher-rank polymorphism : type inference and extensions

Abstract

Type inference, as implemented in various modern programming languages, reconstructs missing types in expressions and increases programmers' productivity. Modern functional languages such as Haskell come with powerful forms of type inference. The global type-inference algorithms employed in those languages are derived from the Hindley-Milner type system, with multiple extensions. As the languages evolve, researchers also formalize the key aspects of type inference for the new extensions.

This dissertation studies predicative implicit higher-rank polymorphism, where polymorphic types can be arbitrarily nested, and monomorphic types can be inferred automatically. Predicative implicit higher-rank polymorphism is a common extension that has been studied extensively in the literature, and has been used pervasively in modern statically typed programming languages.

The goal of this dissertation is to explore the design space of type inference for implicit predicative higher-rank polymorphism, as well as to study its integration with other advanced type system features. The first contribution of this dissertation is a new type inference algorithm for implicit higher-rank polymorphism which can accepts programs that many existing type inference algorithms cannot. The proposed application mode provides new insights for bidirectional type checking. The second contribution is the first combination of predicative implicit higher-rank polymorphism with gradual typing, which provides a step forward in gradualizing modern functional programming languages. The third contribution is an arguably simpler algorithmic implementation of subtyping for higher-rank polymorphism. The technique developed is then further applied to the kind inference problem for datatypes, which provides a first known formal model of datatype declarations in modern functional programming languages.