Flexible types: robust type inference for first-class polymorphism

ABSTRACT

We present HML, a type inference system that supports full first-class 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. A small reference implementation with many examples is available at: http://research.microsoft.com/users/daan/pubs.html.

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: George Kuan , David MacQueen, Efficient type inference using ranked type variables, Proceedings of the 2007 workshop on Workshop on ML, October 05-05, 2007, Freiburg, Germany [doi>10.1145/1292535.1292538]
• 9: Didier Le Botlan. MLF: 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´emy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
• 12: Daan Leijen, HMF: simple type inference for first-class polymorphism, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 13: Daan Leijen. A reference implementation of HML. Available at http://research.microsoft.com/users/daan/pubs. html, April 2008b.
• 14: 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
• 15: 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
• 16: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:248--375, 1978.
• 17: 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]
• 18: 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]
• 19: 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
• 20: 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]
• 21: 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
• 22: 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
• 23: 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, mlf, system f