Automatic discovery of covariant read-only fields

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: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 3: Marcin Benke, Efficient Type Reconstruction in the Presence of Inheritance, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.272-280, August 30-September 03, 1993
• 4: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 5: Michele Bugliesi , Santiago M. Pericás-Geertsen, Type inference for variant object types, Information and Computation, v.177 n.1, p.2-27, 25 August 2002 [doi>10.1006/inco.2002.3091]
• 6: Alexandre Frey, Satisfying Subtype Inequalities in Polynomial Space, Proceedings of the 4th International Symposium on Static Analysis, p.265-277, September 08-10, 1997
• 7: Neal Glew, An efficient class and object encoding, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.311-324, October 2000, Minneapolis, Minnesota, United States
• 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: My Hoang , John C. Mitchell, Lower bounds on type inference with subtypes, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.176-185, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199481]
• 10: Atsushi Igarashi , Naoki Kobayashi, Type reconstruction for linear &pgr;-calculus with I/O subtyping, Information and Computation, v.161 n.1, p.1-44, Aug. 25, 2000 [doi>10.1006/inco.2000.2872]
• 11: Atsushi Igarashi , Mirko Viroli, On Variance-Based Subtyping for Parametric Types, Proceedings of the 16th European Conference on Object-Oriented Programming, p.441-469, June 10-14, 2002
• 12: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, v.49 n.2, p.306-324, Oct. 1994 [doi>10.1016/S0022-0000(05)80051-0]
• 13: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 14: David McAllester, On the complexity analysis of static analyses, Journal of the ACM (JACM), v.49 n.4, p.512-537, July 2002 [doi>10.1145/581771.581774]
• 15: Robin Milner, Operational and algebraic semantics of concurrent processes, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 16: Robin Milner , Mads Tofte, Co-induction in relational semantics, Theoretical Computer Science, v.87 n.1, p.209-220, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90033-X]
• 17: Mitchell, J. C.1991. Type inference with simple subtypes. J. Funct. Prog. 1, 245--285.
• 18: Martin Müller , Joachim Niehren , Andreas Podelski, Ordering Constraints over Feature Trees, Constraints, v.5 n.1-2, p.7-41, January 2000 [doi>10.1023/A:1009866317252]
• 19: Flemming Nielson, The Typed lambda-Calculus with First-Class Processes, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.357-373, June 12-16, 1989
• 20: Jens Palsberg, Efficient inference of object types, Information and Computation, v.123 n.2, p.198-209, Dec. 1995 [doi>10.1006/inco.1995.1168]
• 21: Jens Palsberg , Trevor Jim, Type inference with simple selftypes is NP-complete, Nordic Journal of Computing, v.4 n.3, p.259-286, Fall 1997
• 22: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-378, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199533]
• 23: Jens Palsberg , Scott Smith, Constrained types and their expressiveness, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.5, p.519-527, Sept. 1996 [doi>10.1145/232706.232715]
• 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: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 27: François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 28: Didier Rémy, From Classes to Objects via Subtyping, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.200-220, March 28-April 04, 1998
• 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: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Languages, Theory

Keywords:
Types, constraints