HMF: simple type inference for first-class polymorphism

ABSTRACT

HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm W. Given the relative simplicity and expressive power, we feel that HMF can be an attractive type system in practice. There is a reference implementation of the type system available online together with a technical report containing proofs (Leijen 2007a,b).

REFERENCES

• 1: H. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, 1958.
• 2: Luis Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, April 1985. Technical report CST-33-85.
• 3: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 4: Atze Dijkstra. Stepping through Haskell. PhD thesis, Universiteit Utrecht, Nov. 2005.
• 5: Jacques Garrigue , Didier Rémy, Semi-explicit first-class polymorphism for ML, Information and Computation, v.155 n.1-2, p.134-169, Nov./Dec. 1999 [doi>10.1006/inco.1999.2830]
• 6: J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29--60, Dec. 1969.
• 7: Mark P. Jones, First-class polymorphism with type inference, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.483-496, January 15-17, 1997, Paris, France [doi>10.1145/263699.263765]
• 8: Mark P. Jones. Formal properties of the Hindley-Milner type system. Unpublished notes, August 1995.
• 9: Didier Le Botlan. ML^F: Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, INRIA Rocquencourt, May 2004. Also in English.
• 10: Didier Le Botlan , Didier Rémy, ML^F: raising ML to the power of system F, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.27-38, August 25-29, 2003, Uppsala, Sweden
• 11: Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, France, June 2007.
• 12: Daan Leijen. A reference implementation of HMF. Available at http://research.microsoft.com/users/daan/pubs.html, September 2007a.
• 13: Daan Leijen. HMF: Simple type inference for first-class polymorphism. Technical Report MSR-TR-2007-118, Microsoft Research, September 2007b. Extended version with proofs.
• 14: Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008.
• 15: Daan Leijen, A type directed translation of MLF to system F, Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 16: Daan Leijen , Andres Löh, Qualified types for MLF, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 17: Xavier Leroy , Michel Mauny, Dynamics in ML, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.406-426, August 26-30, 1991
• 18: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:248--375, 1978.
• 19: Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237729]
• 20: Simon Peyton Jones and Mark Shields. Lexically scoped type variables. Draft, March 2004.
• 21: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Mark Shields, Practical type inference for arbitrary-rank types, Journal of Functional Programming, v.17 n.1, p.1-82, January 2007 [doi>10.1017/S0956796806006034]
• 22: Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
• 23: Didier Rémy, Simple, partial type-inference for System F based on type-containment, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 24: Didier Rémy , Boris Yakobowski, A graphical presentation of ML^F types with a linear-time unification algorithm, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190321]
• 25: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 26: Dimitrios Vytiniotis , Stephanie Weirich , Simon Peyton Jones, Boxy types: inference for higher-rank types and impredicativity, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 27: Dimitrios Vytiniotis , Stephanie Weirich , Simon Peyton Jones, FPH: first-class polymorphism for Haskell, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 28: J.B.Wells. Typability and type checking in System-F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1-3):111--156,1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

General Terms:
Design, Languages, Theory

Keywords:
first-class polymorphism, type inference