A Type Directed Translation from MLF to System F
Proceedings of the ACM International Conference on Functional Programming (ICFP'07) |
Published by ACM SIGPLAN
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.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM's Digital Library --http://www.acm.org/dl/.