Type Inference for First-Class Messages with Feature Constraints

  • Martin Müller
  • Susumu Nishimura
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)


We present a constraint system OF of feature trees that is appropriate to specify and implement type inference for first-class messages. OF extends traditional systems of feature constraints by a selection constraint x[y]z “by first-class feature tree” y, in contrast to the standard selection constraint x[f]y “by fixed feature” f. We investigate the satisfiability problem of OF and show that it can be solved in polynomial time, and even in quadratic time in an important special case. We compare OF with Treinen’s constraint system EF of feature constraints with first-class features, which has an NP-complete satisfiability problem. This comparison yields that the satisfiability problem for OF with negation is NP-hard. Based on OF we give a simple account of type inference for first-class messages in the spirit of Nishimura’s recent proposal, and we show that it has polynomial time complexity: We also highlight an immediate extension that is desirable but makes type inference NP-hard.


object-oriented programming first-class messages constraint-based type inference complexity feature constraints 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Aiken and E. Wimmers. Type inclusion constraints and type inference. iIn Proceedings of the 6 th ACM Conference on Functional Programming and Computer Architecture, pp. 31–41. ACM Press, New York, June 1993.CrossRefGoogle Scholar
  2. 2.
    H. Aït-Kaci and A. Podelski. Towards a meaning of life. The Journal of Logic Programming, 16(3-4):195–234, July, Aug. 1993.Google Scholar
  3. 3.
    H. Aït-Kaci, A. Podelski, and G. Smolka. A feature-based constraint system for logic programming with entailment. Theoretical Computer Science, 122(1-2):263–283, Jan. 1994.Google Scholar
  4. 4.
    R. Backofen. A complete axiomatization of a theory with feature and arity constraints. The Journal of Logic Programming, 24(1-2):37–71, 1995. Special Issue onComputational Linguistics and Logic Programming.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    R. Backofen and G. Smolka. A complete and recursive feature theory. Theoretical Computer Science, 146(1-2):243–268, July 1995.Google Scholar
  6. 6.
    F. Bourdoncle and S. Merz. Type checking higher-order polymorphic multimethods. In Proceedings of the 24 th ACM Symposium on Principles of Programming Languages, pp. 302–315. ACM Press, New York, Jan. 1997.CrossRefGoogle Scholar
  7. 7.
    M. Dietzfelbinger, A. Karlin, K. Mehlhorn, F. Meyer Auf Der Heide, H. Rohnert, and R. E. Tarjan. Dynamic perfect hashing: Upper and lower bounds. SIAM Journal of Computing, 23(4):738–761, Aug. 1994.Google Scholar
  8. 8.
    J. Eifrig, S. Smith, and V. Trifonow. Type inference for recursively constrained types and its application to object-oriented programming. Electronic Notes in Theoretical Computer Science, 1, 1995.Google Scholar
  9. 9.
    M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, New York, 1979.zbMATHGoogle Scholar
  10. 10.
    R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, Dec. 1969.Google Scholar
  11. 11.
    H. G. Mairson. Deciding ML typebility is complete for deterministic exponential time. In Proceedings of the 17 th ACM Symposium on Principles of Programming Languages, pp. 382–401. ACM Press, New York, Jan. 1990.CrossRefGoogle Scholar
  12. 12.
    K. Mehlhorn and P. Tsakalides. Data structures. In van Leeuwen [31], chapter 6, pp. 301–342.Google Scholar
  13. 13.
    R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Science, 17(3):348–375, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, MA, 1997.Google Scholar
  15. 15.
    M. Müller, J. Niehren, and A. Podelski. Inclusion constraints over non-empty sets of trees. In M. Bidoit and M. Dauchet, eds., Proceedings of the Theory and Practice of Software Development, vol. 1214 of Lecture Notes in Computer Science, pp. 345–356. Springer-Verlag, Berlin, Apr. 1997.CrossRefGoogle Scholar
  16. 16.
    M. Müller, J. Niehren, and A. Podelski. Ordering constraints over feature trees. In G. Smolka, ed., Proceedings of the 3 rd International Conference on Principles and Practice of Constraint Programming, vol. 1330 of Lecture Notes in Computer Science, pp. 297–311. Springer-Verlag, Berlin, 1997. Full version submitted to special journal issue of CP’97.Google Scholar
  17. 17.
    M. Müller and S. Nishimura. Type inference for first-class messages with feature constraints. Technical report, Programming Systems Lab, Universität des Saarlandes, 1998.
  18. 18.
    S. Nishimura. Static typing for dynamic messages. In Proceedings of the 25 th ACM Symposium on Principles of Programming Languages, pp. 266–278. ACM Press, New York, 1998.CrossRefGoogle Scholar
  19. 19.
    M. Odersky, P. Wadler, and M. Wehr. A second look at overloading. In Proceedings of the 7 th ACM Conference on Functional Programming and Computer Architecture. ACM Press, New York, 1995.Google Scholar
  20. 20.
    A. Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844–895, 1995.CrossRefGoogle Scholar
  21. 21.
    J. Palsberg. Efficient inference of object types. In Proceedings of the 9 th IEEE Symposium on Logic in Computer Science, pp. 186–185. IEEE Computer Society Press, 1994.Google Scholar
  22. 22.
    C. Pollard and I. Sag. Head-Driven Phrase Structure Grammar. Studies in Contemporary Linguistics. Cambridge University Press, Cambridge, England, 1994.Google Scholar
  23. 23.
    D. Rémy. Type checking records and variants in a natural extension of ML. In Proceedings of the 16 th ACM Symposium on Principles of Programming Languages, pp. 77–87. ACM Press, New York, 1989.CrossRefGoogle Scholar
  24. 24.
    D. Rémy and J. Vouillon. Objective ML: A simple object-oriented extension of ML. In Proceedings of the 24 th ACM Symposium on Principles of Programming Languages, pp. 40–53. ACM Press, New York, 1997.CrossRefGoogle Scholar
  25. 25.
    W. C. Rounds. Feature logics. In J. v. Benthem and A. ter Meulen, eds., Handbook of Logic and Language, pp. 475–533. Elsevier Science Publishers B.V. (North Holland), 1997. Part 2: General Topics.Google Scholar
  26. 26.
    G. Smolka. The Oz Programming Model. In J. van Leeuwen, ed., Computer Science Today, vol. 1000 of Lecture Notes in Computer Science, pp. 324–343. Springer-Verlag, Berlin, 1995.CrossRefGoogle Scholar
  27. 27.
    G. Smolka and R. Treinen. Records for logic programming. The Journal of Logic Programming, 18(3):229–258, Apr. 1994.Google Scholar
  28. 28.
    M. Sulzmann. Proofs of properties about HM(X). Technical Report YALEU/DCS/RR-1102, Yale University, 1998.Google Scholar
  29. 29.
    M. Sulzmann, M. Odersky, and M. Wehr. Type inference with constrained types (extended abstract). In B. Pierce, ed., Proceedings of the 4 th International Workshop on Foundations of Object-oriented Programming, Jan. 1997. Full version to appear in TAPOS, 1998.Google Scholar
  30. 30.
    R. Treinen. Feature constraints with first-class features. In A. M. Borzyszkowski and S. Sokolowski, eds., International Symposium on Mathematical Foundations of Computer Science, vol. 711 of Lecture Notes in Computer Science, pp. 734–743. Springer-Verlag, Berlin, 30 August–3 September 1993.Google Scholar
  31. 31.
    J. van Leeuwen, ed. Handbook of Theoretical Computer Science, vol. A (Algorithms and Complexity). The MIT Press, Cambridge, MA, 1990.Google Scholar
  32. 32.
    M. Wand. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 37–44. IEEE Computer Society Press, 1987. Corrigendum in LICS’ 88, p. 132.Google Scholar
  33. 33.
    M. Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93:1–15, 1991.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Martin Müller
    • 1
  • Susumu Nishimura
    • 2
  1. 1.Universität des SaarlandesSaarbrückenGermany
  2. 2.RIMSKyoto UniversityKyotoJapan

Personalised recommendations