First-class Polymorphism

Type inference systems for functional languages are usually based on Hindley-Milner, where polymorphism is restricted to let-bound values only. An long standing research challenge is to do type inference for full System-F where polymorphism is first-class and where polymorphic values can be passed as arguments or be part of data structures. Since type inference for System-F is undecidable in general, the question is how to use the minimal amount of annotations to still do predicatable inference.

The following papers on HML and HMF both describe two interesting corners in the design space of type inference systems for first-class polymorphism:

  • The MLF system (by Didier Remy and Didier LeBotlan) represents an upper bound: it arguably requires the least annotations possible while being very expressive (it requires only annotations on function parameters that are used polymorphically). However, it is also the most complex using rigidly bound types and a relatively involved type inference algorithm.
  • The HMF paper describes a lower bound in the design space: it uses just regular System-F types and type inference is just a small extension of the usual algorithm W. It is a lower bound in the sense that it would be hard to come up with a simpler system that has the same expressiveness without requiring more annotations. This is the system you would use if you want first-class polymorphism with minimal implementation effort. There is a reference implementation of the type system written in Haskell that contains many examples. It is available in two variants, one using updateable references (prototype-ref), and one using explicit substitutions (prototype-subst).
  • The Flexible types paper (or HML) describes a type system that lies between these design points: it is a simplification of MLF that uses just flexible types and it has a very simple annotation rule: only function parameters that are polymorphic need an annotation. It is arguably the most expressive system possible when using types with flexible bounds only. This is the system you would use if you want powerful support for first-class polymorphism and are willing to put more effort into the implementation.

    There is a small but complete reference implementation of the type system written in Haskell that contains many examples.

Publications
  • Daan Leijen, Flexible types: robust type inference for first-class polymorphism, in 36th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'09), ACM SIGPLAN, Savannah, Georgia, January 2009

    We present HML, a type inference system that supports full firstclass polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified types are used. This makes the types easier to work with from a programmers perspective, and simplifies the implementation of the type inference algorithm. Still, HML retains much of the expressiveness of MLF, it is robust with respect to small program transformations, and has a simple specification of the type rules with an effective type inference algorithm that infers principal types.

    Extended version available as Microsoft Research technical report MSR-TR-2008-55, Mar 2008 (see link below)

  • Daan Leijen, HMF: Simple Type Inference for First-Class Polymorphism, in 13th ACM symp. of the International Conference on Functional Programming (ICFP'08), Association for Computing Machinery, Inc., Victoria, BC, Canada, September 2008

    HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism and regular System F types. The system distinguishes itself from other proposals with simple type rules and a very simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm. Given the relative simplicity and expressive power, we feel that HMF can be a very attractive type system in practice.

    Extended version with proofs available as Microsoft Research technical report MSR-TR-2007-118, Sep 2007 (see link below)

  • Daan Leijen, Flexible types: robust type inference for first-class polymorphism, no. MSR-TR-2008-55, March 2008
  • Daan Leijen, HMF: Simple Type Inference for First-Class Polymorphism, no. MSR-TR-2007-118, 30 October 2007
  • Daan Leijen, A Type Directed Translation from MLF to System F, in Proceedings of the ACM International Conference on Functional Programming (ICFP'07), ACM SIGPLAN, Freiburg, Germany, 1 October 2007

    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.

  • Daan Leijen and Andres Löh, Qualified types for MLF, in The International Conference on Functional Programming (ICFP'05), ACM SIGPLAN, Tallin, Estonia, September 2005

    ML-F is a type system that extends a functional language with impredicative higher-rank polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that can accomodate a wide range of type systems extension, for example, type classes in Haskell. We show how the theory of qualified types can be used seamlessly with the higher-ranked impredicative polymorphism of ML-F. A core contribution of the paper is that we show a solution to the non-trivial problem of evidence translation in the presence of impredicative data types. (Note: one can experiment with MLF types with the experimental Morrow interpreter. However, this does not yet implement the qualified type extension discussed in the paper)