Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
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.
R. Backofen and G. Smolka. A complete and recursive feature theory. Theoretical Computer Science, 146(1-2):243–268, July 1995.
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.
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.
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.
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.
R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, Dec. 1969.
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.
K. Mehlhorn and P. Tsakalides. Data structures. In van Leeuwen [31], chapter 6, pp. 301–342.
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Science, 17(3):348–375, 1978.
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, MA, 1997.
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.
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.
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. http://www.ps.uni-sb.de/Papers/abstracts/FirstClass98.html
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.
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.
A. Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844–895, 1995.
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.
C. Pollard and I. Sag. Head-Driven Phrase Structure Grammar. Studies in Contemporary Linguistics. Cambridge University Press, Cambridge, England, 1994.
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.
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.
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.
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.
G. Smolka and R. Treinen. Records for logic programming. The Journal of Logic Programming, 18(3):229–258, Apr. 1994.
M. Sulzmann. Proofs of properties about HM(X). Technical Report YALEU/DCS/RR-1102, Yale University, 1998.
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.
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.
J. van Leeuwen, ed. Handbook of Theoretical Computer Science, vol. A (Algorithms and Complexity). The MIT Press, Cambridge, MA, 1990.
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.
M. Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93:1–15, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, M., Nishimura, S. (1998). Type Inference for First-Class Messages with Feature Constraints. In: Hsiang, J., Ohori, A. (eds) Advances in Computing Science ASIAN 98. ASIAN 1998. Lecture Notes in Computer Science, vol 1538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49366-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-49366-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65388-2
Online ISBN: 978-3-540-49366-2
eBook Packages: Springer Book Archive