Constrained types and their expressiveness

ABSTRACT

A constrained type consists of both a standard type and a constraint set. Such types enable efficient type inference for object-oriented languages with polymorphism and subtyping, as demonstrated by Eifrig, Smith, and Trifonov. Until now, it has been unclear how expressive constrained types are. In this article we study constrained types without universal quantification. We prove that they accept the same programs as the type system of Amadio and Cardelli with subtyping and recursive types. This result gives a precise connection between constrained types and the standard notion of types.

REFERENCES

• 1: 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]
• 2: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 3: Curtis, P. 1990. Constrained quantification in polymorphic type analysis. Tech. Rep. CSL-90-1, XEROX Palo Alto Research Center, Palo Alto, Calif.
• 4: Jonathan Eifrig , Scott Smith , Valery Trifonov, Sound polymorphic type inference for objects, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.169-184, October 15-19, 1995, Austin, Texas, United States
• 5: Eifrig, J., Smith, S., and Trifonov, V. 1995b. Type inference for recursively constrained types and it application to OOP. In Proceedings of Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier Science B.V., New York.
• 6: Stefan Kaes, Type inference in the presence of overloading, subtyping and recursive types, Proceedings of the 1992 ACM conference on LISP and functional programming, p.193-204, June 22-24, 1992, San Francisco, California, United States
• 7: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient recursive subtyping, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.419-428, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158700]
• 8: Mitchell, J. C. 1991. Type inference with simple subtypes. J. Funct. Program. 1, 245-285.
• 9: 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]

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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

General Terms:
Languages, Theory

Keywords:
constraints