FPH: first-class polymorphism for Haskell

ABSTRACT

Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting "firstclass" polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.

REFERENCES

• 1: 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]
• 2: 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]
• 3: A. J. Kfoury , J. B. Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order &lgr;-calculus, Proceedings of the 1994 ACM conference on LISP and functional programming, p.196-207, June 27-29, 1994, Orlando, Florida, United States
• 4: 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
• 5: Didier Le Botlan. MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, Ecole Polytechnique, May 2004. 326 pages, also available in english.
• 6: Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
• 7: 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
• 8: Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008b.
• 9: 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
• 10: 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
• 11: R Milner. A theory of type polymorphism in programming. JCSS, 13(3), December 1978.
• 12: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 13: 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]
• 14: 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]
• 15: Frank Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.153-163, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62697]
• 16: 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
• 17: Dimitrios Vytiniotis. Practical type inference for first-class polymorphism. PhD thesis, University of Pennsylvania, 2008. URL www.cis.upenn.edu/~dimitriv/fph. In submission.
• 18: 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
• 19: JB Wells. Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic, 98:111--156, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

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

General Terms:
Languages, Theory

Keywords:
higher-rank types, impredicativity, type inference