A direct algorithm for type inference in the rank-2 fragment of the second-order &lgr;-calculus

ABSTRACT

We examine the problem of type inference for a family of polymorphic type systems containing the power of Core-ML. This family comprises the levels of the stratification of the second-order &lgr;-calculus (system F) by “rank” of types. We show that typability is an undecidable problem at every rank k≥3. While it was already known that typability is decidable at rank 2, no direct and easy-to-implement algorithm was available. We develop a new notion of &lgr;-term reduction and use it to prove that the problem of typability at rank 2 is reducible to the problem of acyclic semi-unification. We also describe a simple procedure for solving acyclic semi-unification. Issues related to principle types are discussed.

REFERENCES

• Dow93: Gilles Dowek, The Undecidability of Typability in the Lambda-Pi-Calculus, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.139-145, March 16-18, 1993
• Gir72: J.-Y. Girard. interpretation Fonctionn~lle et Elimination des Coupures de i'Arithm4tique d'Ordre $up4rieur, Th~se d'Etat, Universit~ Paris VII, 1972.
• GMW79: M. J. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF, vol. 78 of LNCS. Springer- Verlag, 1979.
• GRDR91: Paola Giannini , Simona Ronchi Della Rocca, Type Inference in Polymorphic Type Discipline, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.18-37, September 24-27, 1991
• Hen88: Fritz Henglein, Type inference and semi-unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.184-197, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62701]
• HW88: P. Hudak and P. L. Wadler. Report on the functional programming language Haskell. Technical Report YALEU/DCS/RR656, Yale University, 1988.
• KMM90: P. Kanellakis, H. Mairson, and J. C. Mitchell. Unification and ML type reconstruction. In Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1990.
• KT92: A. J. Kfoury , J. Tiuryn, Type reconstruction in finite rank fragments of the second-order &lgr;-calculus, Information and Computation, v.98 n.2, p.228-257, June 1992 [doi>10.1016/0890-5401(92)90020-G]
• KTU90: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, ML typability is Dexptime-complete, Proceedings of the fifteenth colloquium on CAAP'90, p.206-220, May 1990, Copenhagen, Denmark
• KTU93: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Information and Computation, v.102 n.1, p.83-101, Jan. 1993 [doi>10.1006/inco.1993.1003]
• Lei83: Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567077]
• Lei91: Daniel Leivant, Finitely stratified polymorphism, Information and Computation, v.93 n.1, p.93-113, July 1991 [doi>10.1016/0890-5401(91)90053-5]
• McC84: Nancy McCracken, The typechecking of programs with implicit type structure., Proc. of the international symposium on Semantics of data types, p.301-315, July 1984, Sophia-Antipolis, France
• Mil85: R. Milner. The standard ML core language. Polymorphism, 2(2), Oct. 1985.
• Pie92: Benjamin C. Pierce, Bounded quantification is undecidable, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.305-315, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143228]
• Rey74: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• Tiu90: Jerzy Tiuryn, Type inference problems: a survey, Proceedings on Mathematical foundations of computer science 1990, p.105-120, September 1990, Banska´ Bystrica, Czechoslovakia
• TLCA93: lnt'l Conf. Typed Lambda Calculi and Applications, vol. 664 of LNCS. Springer-Verlag, Mar. 1993.
• Tur85: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France
• Urz93: Pawel Urzyczyn, Type reconstruction in F-omega is undecidable, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.418-432, March 16-18, 1993
• Wel93: J. B. Wells, Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable, Boston University, Boston, MA, 1993

INDEX TERMS

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

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Theory