A Type Directed Translation from MLF to System F

Daan Leijen

Abstract

The MLF type system by Le Botlan and Rémy (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.

Details

Publication typeInproceedings
Published inProceedings of the ACM International Conference on Functional Programming (ICFP'07)
AddressFreiburg, Germany
PublisherACM SIGPLAN
> Publications > A Type Directed Translation from MLF to System F