Lower bounds on type inference with subtypes

ABSTRACT

We investigate type inference for programming languages with subtypes. As described in previous work, there are several type inference problems for any given expression language, depending on the form of the subtype partial order and the ability to define new subtypes in programs. Our first main result is that for any specific subtype partial order, the problem of determining whether a lambda term is typable is algorithmically (polynomial-time) equivalent to a form of satisfiability problem over the same partial order. This gives the first exact characterization of the problem that is independent of the syntax of expressions. In addition, since this form of satisfiability problem is PSPACE-hard over certain partial orders, this equivalence strengthens the previous lower bound of NP-hard to PSPACE-hard. Our second main result is a lower bound on the length of most general types when the subtype hierarchy may change as a result of additional type declarations within the program. More specifically, given any input expression, a type inference algorithm tries to find a most general (or principal) typing. The property of a most general typing is that it has all other possible typings as instances. However, there are several sound notions of instance in the presence of subtyping. Our lower bound is that no sound definition of instance would allow the set of additional subtyping hypotheses about a term to grow less than linearly in the size of the term.

REFERENCES

• ASU86: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• Ben94: M. Benke. Efficient type reconstruction in the presence of inheritance. Manuscript, 1994.
• FM89: You-Chin Fuh , Prateek Mishra, Polymorphic Subtype Inference: Closing the Theory-Practice Gap, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.167-183, March 13-17, 1989
• FM90: You-Chin Fuh , Prateek Mishra, Type inference with subtypes, Theoretical Computer Science, v.73 n.2, p.155-175, June 22, 1990
• GMW79: M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Springer LNCS 78, Berlin, 1979.
• H+92: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• HF92: Paul Hudak , Joseph H. Fasel, A gentle introduction to Haskell, ACM SIGPLAN Notices, v.27 n.5, p.1-52, May 1992 [doi>10.1145/130697.130698]
• LM92: Patrick Lincoln , John C. Mitchell, Algorithmic aspects of type inference with subtypes, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.293-304, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143227]
• Mil85: R. Milner. The Standard ML core language. Polymorphism, 2(2), 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.
• Mit84: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• Mit91a: J.C. Mitchell. A simple reduction of unification to typability. Message to [e-mail], June 28 1991.
• Mit91b: J.C. Mitchell. Type inference with simple subtypes. J. Functional Programming, 1(3):245-286, 1991.
• PT91: V. Pratt and J. Tiuryn. Satisfiability of inequations in a poset. Manuscript, October 1991.
• Tiu91: J. Tiuryn. Solving term inequalities is PSPACE- hard. Manuscript, October 1991.
• Tiu92: J. Tiuryn. Subtype inequalities. In Proc. IEEE Symp. on Logic in Computer Science, pages 308- 315, 1992.
• 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
• Tys88: J. Tyszkiewicz. Complexity of type inference in finitely typed lambda calculus. Master's thesis, University of Warsaw, 1988.
• Wan87: M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, 10:115-122, 1987.
• WO89: Mitchell Wand , Patrick O'Keefe, On the complexity of type inference with coercion, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.293-298, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99394]

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.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Languages, Theory, Verification