article

Open access

Automatic discovery of covariant read-only fields

Authors:

Trevor JimAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 27, Issue 1

Pages 126 - 162

https://doi.org/10.1145/1053468.1053472

Published: 01 January 2005 Publication History

Abstract

Read-only fields are useful in object calculi, pi calculi, and statically typed intermediate languages because they admit covariant subtyping, unlike updateable fields. For example, Glew's translation of classes and objects to an intermediate calculus relies crucially on covariant subtyping of read-only fields to ensure that subclasses are translated to subtypes.In this article, we present a type inference algorithm for an Abadi--Cardelli object calculus in which fields are marked either as updateable or as read-only. The type inference problem is P-complete, and our algorithm runs in O(n³) time. The same complexity results hold for the calculus in which the fields are not explicitly annotated as updateable or read-only; perhaps surprisingly, the annotations do not make type inference easier. We show that type inference is equivalent to the problem of solving type constraints, and this forms the core of our algorithm and implementation.

References

[1]

Abadi, M. and Cardelli, L.1996. A Theory of Objects. Springer-Verlag, New York.

[2]

Aiken, A. and Wimmers, E.1993. Type inclusion constraints and type inference. In Proceedings of Conference on Functional Programming Languages and Computer Architecture. pp. 31--41.

[3]

Benke, M.1993. Efficient type reconstruction in the presence of inheritance. In Proceedings of Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, New York, 272--280.

[4]

Bracha, G., Odersky, M., Stoutamire, D., and Wadler, P.1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of OOPSLA'98, ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. ACM, New York, pp. 183--200.

[5]

Bugliesi, M. and Pericas-Geertsen, S.2002. Type inference for variant object types. Inf. Comput. 177, 1, 2--27.

[6]

Frey, A.1997. Satisfying systems of subtype inequalities in polynomial space. In Proceedings of SAS'97, International Static Analysis Symposium. Lecture Notes in Computer Science. Springer-Verlag, New York.

[7]

Glew, N.2000. An efficient class and object encoding. In Proceedings of OOPSLA'00, ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (Minneapolis, Minn. Oct.). ACM, New York, pp. 311--324.

[8]

Henglein, F.1997. Breaking through the n3 barrier: Faster object type inference. In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages. http://www.cs.williams.edu/kim/FOOL/index.html.

[9]

Hoang, M. and Mitchell, J. C.1995. Lower bounds on type inference with subtypes. In Proceedings of POPL'95, 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages. ACM, New York, pp. 176--185.

[10]

Igarashi, A. and Kobayashi, N.2000 Type reconstruction for linear pi-calculus with I/O subtyping. Inf. Comput., 161, 1, 1--44.

[11]

Igarashi, A. and Viroli, M.2002. On variance-based subtyping for parametric types. In Proceedings of ECOOP'02, 16th European Conference on Object-Oriented Programming.

[12]

Kozen, D., Palsberg, J., and Schwartzbach, M. I.1994. Efficient inference of partial types. J. Comput. Syst. Sci. 49, 2, 306--324. Preliminary version in Proceedings of FOCS'92, 33rd IEEE Symposium on Foundations of Computer Science (Pittsburgh, Pa., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 363--371.

[13]

MacQueen, D., Plotkin, G., and Sethi, R.1986. An ideal model for recursive polymorphic types. Inf. Comput. 71, 1/2 (Oct./Nov.), 95--130.

[14]

McAllester, D.2002. On the complexity analysis of static analyses. J. ACM 49, 4, 512--537.

[15]

Milner, R.1990. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Chap. 19, J. van Leewen, Ed. The MIT Press, New York, N.Y., pp. 1201--1242.

[16]

Milner, R. and Tofte, M.1991. Co-induction in relational semantics. Theoret. Comput. Sci. 87, 1, 209--220.

[17]

Mitchell, J. C.1991. Type inference with simple subtypes. J. Funct. Prog. 1, 245--285.

[18]

Müller, M., Niehren, J., and Podelski, A.2000. Ordering constraints over feature trees. Constr. Internat. J. 5, 1--2 (Jan.), 7--42.

[19]

Nielson, F.1989. The typed lambda-calculus with first-class processes. In Proceedings of PARLE'89. pp. 357--373.

[20]

Palsberg, J.1995. Efficient inference of object types. Inf. Comput. 123, 2, 198--209. (Preliminary version in Proceedings of LICS'94, Ninth Annual IEEE Symposium on Logic in Computer Science (Paris, France, July 1994), pp. 186--195.)

[21]

Palsberg, J. and Jim, T.1997. Type inference with simple selftypes is NP-complete. Nord. J. Comput. 4, 3, 259--286.

[22]

Palsberg, J. and O'Keefe, P. M.1995. A type system equivalent to flow analysis. ACM Trans. Prog. Lang. Syst. 17, 4 (July), 576--599. (Preliminary version in Proceedings of POPL'95, 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages (San Francisco, Calif., Jan. 1995), pp. 367--378.)

[23]

Palsberg, J. and Smith, S.1996. Constrained types and their expressiveness. ACM Trans. Prog. Lang. Syst. 18, 5 (Sept.), 519--527.

[24]

Palsberg, J., Wand, M., and O'Keefe, P. M.1997. Type inference with non-structural subtyping. Form. Asp. Comput. 9, 49--67.

[25]

Pierce, B. and Sangiorgi, D.1993. Typing and subtyping for mobile processes. In Annual Symposium on Logic in Computer Science (LICS'93), pp. 376--385.

[26]

Pierce, B. C.2002. Types and Programming Languages. MIT Press, Cambridge, Mass.

[27]

Pottier, F.1996. Simplifying subtyping constraints. In Proceedings of ACM SIGPLAN International Conference on Functional Programming. ACM, New York, pp. 122--133.

[28]

Rémy, D.1998. From classes to objects via subtyping. In Proceedings of the European Symposium on Programming (Mar.). Lecture Notes in Computer Science, vol. 1381. Springer-Verlag, New York.

[29]

Sulzmann, M., Müller, M., and Zenger, C.1999. Hindley/Milner style type systems in constraint form. Tech. Rep. ACRC-99-009. University of South Australia.

[30]

Tang, F. and Hofmann, M.2001. Type inference for objects with base types. Draft.

[31]

Tang, F. and Hofmann, M.2002. Generation of verification conditions for Abadi and Leino's logic of objects. In Proceedings of FOOL'02, Ninth International Workshop on Foundations of Object-Oriented Languages (Portland, Ore., Jan.).

[32]

Tiuryn, J.1992. Subtype inequalities. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS'92). IEEE Computer Society Press, Los Alamitos, Calif., pp. 308--315.

[33]

Wand, M., O'Keefe, P. M., and Palsberg, J.1995. Strong normalization with non-structural subtyping. Math. Struct. Comput. Sci. 5, 3, 419--430.

[34]

Wright, A. and Felleisen, M.1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38--94.

Cited By

Zhao T(2011)Polymorphic type inference for scripting languages with object extensionsACM SIGPLAN Notices10.1145/2168696.204785547:2(37-50)Online publication date: 24-Oct-2011
https://dl.acm.org/doi/10.1145/2168696.2047855
Zhao TD'Hondt T(2011)Polymorphic type inference for scripting languages with object extensionsProceedings of the 7th symposium on Dynamic languages10.1145/2047849.2047855(37-50)Online publication date: 24-Oct-2011
https://dl.acm.org/doi/10.1145/2047849.2047855

Index Terms

Automatic discovery of covariant read-only fields
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Flow-insensitive type qualifiers

We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming ...
Constrained kinds
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

Modern object-oriented languages such as X10 require a rich framework for types capable of expressing both value-dependency and genericity, and supporting pluggable, domain-specific extensions. In earlier work, we presented a framework for constrained ...
Flow-sensitive type qualifiers
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 27, Issue 1

January 2005

184 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1053468

Issue’s Table of Contents

Copyright © 2005 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2005

Published in TOPLAS Volume 27, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
403
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)4

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhao T(2011)Polymorphic type inference for scripting languages with object extensionsACM SIGPLAN Notices10.1145/2168696.204785547:2(37-50)Online publication date: 24-Oct-2011
https://dl.acm.org/doi/10.1145/2168696.2047855
Zhao TD'Hondt T(2011)Polymorphic type inference for scripting languages with object extensionsProceedings of the 7th symposium on Dynamic languages10.1145/2047849.2047855(37-50)Online publication date: 24-Oct-2011
https://dl.acm.org/doi/10.1145/2047849.2047855

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents