Algorithmic aspects of type inference with subtypes

ABSTRACT

We study the complexity of type inference for programming languages with subtypes. There are three language variations that effect the problem: (i) basic functions may have polymorphic or more limited types, (ii) the subtype hierarchy may be fixed or vary as a result of subtype declarations within a program, and (iii) the subtype hierarchy may be an arbitrary partial order or may have a more restricted form, such as a tree or lattice. The naive algorithm for infering a most general polymorphic type, undervariable subtype hypotheses, requires deterministic exponential time. If we fix the subtype ordering, this upper bound grows to nondeterministic exponential time. We show that it is NP-hard to decide whether a lambda term has a type with respect to a fixed subtype hierarchy (involving only atomic type names). This lower bound applies to monomorphic or polymorphic languages. We give PSPACE upper bounds for deciding polymorphic typability if the subtype hierarchy has a lattice structure or the subtype hierarchy varies arbitrarily. We also give a polynomial time algorithm for the limited case where there are of no function constants and the type hierarchy is either variable or any fixed lattice.

REFERENCES

• FM90: You-Chin Fuh , Prateek Mishra, Type inference with subtypes, Theoretical Computer Science, v.73 n.2, p.155-175, June 22, 1990
• Hin89: J. Roger Hindley, BCK-combinators and linear &lgr;-terms have types, Theoretical Computer Science, v.64 n.1, p.97-105, April 1989 [doi>10.1016/0304-3975(89)90100-X]
• Jat89: L. Jategaonkar. ML with extended pattern matching and subtypes. Master's thesis, MIT, 1989.
• JM88: Lalita Jategaonkar , John Mitchell, ML with extended pattern matching and subtypes, Proceedings of the 1988 ACM conference on LISP and functional programming, p.198-211, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62702]
• KMM91: P.C. Kanell~kis, H.G. Mairson, and J.C. Mitchell. Unification and ML type reconstruction. In Computational Logic, essays in honor of Alan Robinson, page to appear. MIT Press, 1991.
• Mey88: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 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]
• Mit91: 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 poser. Manuscript, October 1991.
• PW78: M.S. Paterson and M.N. Wegman. Linear unification. JCSS, 16:158-167, 1978.
• Str86: Bjarne Stroustrup, The C++ programming language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• Tiu91: J. Tiuryn. Solving term inequalities is PSPACE- hard. Manuscript, October 1991.
• Wan87: M. Wand. A simple algorithm and proof for type inference. Fundamcnta Informaticae, 10:115-122, 1987.
• Wan91: M. Wand. Personal communication, 1991.
• 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:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Algorithms, Languages, Verification