MLF: raising ML to the power of system F

Abstract

We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred.All expressions of ML are well-typed without any annotations. All expressions of System F can be mechanically encoded into MLF by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into MLF types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.