From ML to MLF: graphic type constraints with efficient type inference

ABSTRACT

ML^F is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or ML^F. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent ML^F types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for ML^F type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions.

REFERENCES

• 1: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 2: 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
• 3: Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
• 4: 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
• 5: Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008.
• 6: 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
• 7: David McAllester. A logical algorithm for ML type inference. In International Conference on Rewriting Techniques and Applications (RTA), Valencia, Spain, volume 2706 of Lecture Notes in Computer Science, pages 436--451. Springer-Verlag, June 2003.
• 8: François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
• 9: Didier Rémy. Extending ML type system with a sorted equational theory. Research Report 1766, INRIA, 1992.
• 10: 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]
• 11: Didier Rémy and Boris Yakobowski. A Church-style intermediate language for MLF. Submitted, available at http://gallium.inria.fr/~remy/mlf, 2008.
• 12: Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. Extended version, of {10}, September 2008.
• 13: 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
• 14: Joe B.Wells. Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1--3):111--156, 1999.
• 15: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), Victoria, British Columbia, Canada. ACM Press, September 2008.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.3 Language Constructs and Features
          Subjects: Constraints

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
ML, ML^F, binders, graphs, system F, type constraints, type generalization, type inference, type instantiation, types, unification