Type Inference with Rank-1 Restriction
Jimmy
Abstract
Type Inference plays an important role in modern programming language design, as the functional programming style is accepted by more and more programmers. Unfortunately, full type inference on System F is undecidable, being an impredicative and higher-rank system. In practice, predicativity and rank-1 are reasonable restrictions that are adopted by most of the programming languages (the ML family, Haskell, etc.).
Our previous work (ICFP 2019) proposes an algorithm that completely infers types in a predicative higher-rank type system without the support to the top type (object-oriented subtyping). In this seminar talk, I will introduce a new predicative subtyping algorithm that supports the top type with the rank-1 restriction.