A type directed translation of MLF to system F

The MLF type system by Le Botlan and R?emy (2003) is a natural extension of Hindley-Milner type inference that supports full firstclass polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very attractive, it has not seen widespread adoption. We believe that this partly because it is unclear how the rich language of MLF types relate to standard System F types. In this article we give the first type directed translation of MLF terms to System F terms. Based on insight gained from this translation, we also define "Rigid MLF" (MLF= ), a restriction of MLF where all bound values have a System F type. The expressiveness of MLF= is the same as that of boxy types, but MLF= needs fewer annotations and we give a detailed comparison between them. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features--Polymorphism General Terms Languages, Design, Theory Keywords First-class polymo...

• Type: Conference
• Year: 2007
• Where: ICFP
• Authors: Daan Leijen
• Keywords: Hindley-Milner Type Inference, ICFP 2007, Keywords First-class Polymorphism, Programming Languages, Type Directed Translation