MLF: raising ML to the power of system F

We propose a type system MLFthat generalizes ML with first-class polymorphism as in System F. Expressions may contain secondorder 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 welltyped without any annotations. All expressions of System F can be ally encoded into MLF by dropping all type abstractions applications, and injecting types of lambda-abstractions types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated. Categories and Subject Descriptors: D.3.3 Language Constructs and Features. General Terms: Theory, Languages.

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Didier Le Botlan, Didier Rémy
• Keywords: ICFP 2003, Implicit Type Instantiation, Programming Languages, Secondorder Type Annotations, Type Abstractions Applications