Abstract
We develop the mechanism of variant parametric types as a means to enhance synergy between parametric and inclusion polymorphism in object-oriented programming languages. Variant parametric types are used to control both the subtyping between different instantiations of one generic class and the accessibility of their fields and methods. On one hand, one parametric class can be used to derive covariant types, contravariant types, and bivariant types (generally called variant parametric types) by attaching a variance annotation to a type argument. On the other hand, the type system prohibits certain method/field accesses, according to variance annotations, when these accesses may otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions that work on a wide range of parametric types in a safe manner. For instance, a method that only reads the elements of a container of numbers can be easily modified so as to accept containers of integers, floating-point numbers, or any subtype of the number type.Technical subtleties in typing for the proposed mechanism are addressed in terms of an intuitive correspondence between variant parametric and bounded existential types. Then, for a rigorous argument of correctness of the proposed typing rules, we extend Featherweight GJ---an existing formal core calculus for Java with generics---with variant parametric types and prove type soundness.
- Abadi, M., Cardelli, L., and Viswanathan, R. 1996. An interpretation of objects and object types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (St. Petersburg Beach FL), 396--409.]] Google Scholar
- Agesen, O., Freund, S. N., and Mitchell, J. C. 1997. Adding type parameterization to the Java language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Atlanta, GA). 49--65.]] Google Scholar
- America, P. and van der Linden, F. 1990. A parallel object-oriented language with inheritance and subtyping. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications/European Conference on Object-Oriented Programming (OOPSLA/ECOOP) (Ottawa, Canada). 161--168.]] Google Scholar
- Barthe, G. and Frade, M. J. 1999. Constructor subtyping. In Proceedings of the 8th European Symposium on Programming (ESOP) Amsterdam, The Netherlands. Lecture Notes in Computer Science, vol. 1576, Springer Verlag, Berlin, Germany. 109--127.]] Google Scholar
- Barthe, G. and van Raamsdonk, F. 2000. Constructor subtyping in the calculus of inductive constructions. In Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) (Berlin, Germany). Lecture Notes in Computer Science, vol. 1784, Springer Verlag, 17--34.]] Google Scholar
- Bracha, G. 1996. The Strongtalk type system for Smalltalk. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) Workshop on Extending the Smalltalk Language (San Jose, CA). Also available electronically through http://bracha.org/nwst.html.]]Google Scholar
- Bracha, G. and Griswold, D. 1993. Strongtalk: Typechecking Smalltalk in a production environment. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Washington, DC). 215--230.]] Google Scholar
- 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 the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Vancouver, BC). 183--200.]] Google Scholar
- Bruce, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing, and semantics. J. Funct. Program. 4, 2 (Apr.), 127--206. Preliminary version in POPL 1993, under the title “Safe type checking in a statically typed object-oriented programming language.”]] Google Scholar
- Bruce, K. B., Cardelli, L., and Pierce, B. C. 1999. Comparing object encodings. Inf. Comput. 155, 108--133.]] Google Scholar
- Bruce, K. B., Odersky, M., and Wadler, P. 1998. A statically safe alternative to virtual types. In Proceedings of the 12th European Conference on Object-Oriented Programming (ECOOP), Brussels, Belgium. Lecture Notes in Computer Science, vol. 1445. Springer Verlag, 523--549.]] Google Scholar
- Bruce, K. B., Petersen, L., and Fiech, A. 1997. Subtyping is not a good “match” for object-oriented languages. In Proceedings of the 11th European Conference on Object-Oriented Programming (ECOOP) (Jyväskylä, Finland). Lecture Notes in Computer Science, vol. 1241. Springer Verlag, Berlin, Germany, 104--127.]]Google Scholar
- Bruce, K. B., Schuett, A., and van Gent, R. 1995. PolyTOIL: A type-safe polymorphic object-oriented language. In Proceedings of the 9th European Conference on Object-Oriented Programming (ECOOP) (Aarhus, Denmark), W. Olthoff, Ed. Lecture Notes in Computer Science, vol. 952. Springer Verlag, Berlin, Germany 27--51.]] Google Scholar
- Bruce, K. B. and Vanderwaart, J. C. 1999. Semantics-Driven language design: Statically type-safe virtual types in object-oriented languages. In Proceedings of the 15th Conference on the Mathematical Foundations of Programming Semantics (MFPS XV). (New Orleans, LA). Electronic Notes in Theoretical Computer Science, vol. 20. Elsevier. Available through http://www.elsevier.nl/locate/entcs/volume20.html.]]Google Scholar
- Canning, P., Cook, W., Hill, W., Olthoff, W., and Mitchell, J. 1989. F-Bounded quantification for object-oriented programming. In Proceedings of the ACM Conference on Functional Programming and Computer Architecture (FPCA) (London, UK). 273--280.]] Google Scholar
- Cardelli, L. 1990. Notes about Fω<:. Unpublished manuscript.]]Google Scholar
- Cardelli, L., Martini, S., Mitchell, J. C., and Scedrov, A. 1994. An extension of system F with subtyping. Inf. Comput. 109, 1--2, 4--56. LNCS vol. 526. 750--770.]] Google Scholar
- Cardelli, L. and Wegner, P. 1985. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17, 4 (Dec.), 471--522.]] Google Scholar
- Cartwright, R. and Steele Jr., G. L. 1998. Compatible genericity with runtime types for the Java programming language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Vancouver, BC). 201--215.]] Google Scholar
- Compagnoni, A. B. and Pierce, B. C. 1996. Higher-Order intersection types and multiple inheritance. Math. Struct. Comput. Sci. 6, 469--501.]]Google Scholar
- Cook, W. 1989. A proposal for making Eiffel type-safe. In Proceedings of the 3rd European Conference on Object-Oriented Programming (ECOOP) (Nottingham, UK). 57--70.]]Google Scholar
- Day, M., Gruber, R., Liskov, B., and Myers, A. C. 1995. Subtypes vs. where clauses: Constraining parametric polymorphism. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Austin, TX). 156--168.]] Google Scholar
- Duggan, D. and Compagnoni, A. 1999. Subtyping for object type constructors. In Informal Proceedings of the 6th International Workshop on Foundations of Object-Oriented Languages (FOOL6) (San Antonio, TX). Available through http://www.research.att.com/~kfisher/FOOL/FOOL6.html.]]Google Scholar
- Ghelli, G. and Pierce, B. 1998. Bounded existentials and minimal typing. Theor. Comput. Sci. 193, 75--96.]] Google Scholar
- Harper, R. and Lillibridge, M. 1994. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (Portland, OR). 123--137.]] Google Scholar
- Igarashi, A. and Pierce, B. C. 2002. Foundations for virtual types. Inf. Comput. 175, 1 (May), 34--49. An earlier version appeared in Proceedings of the European Conference on Object-Oriented Programming (ECOOP). LNCS 1628, 161--185.]] Google Scholar
- Igarashi, A., Pierce, B. C., and Wadler, P. 2001a. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23, 3 (May), 396--450. A preliminary summary appeared in Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99) (Denver, CO). ACM SIGPLAN Notices 34, 10, 132--146.]] Google Scholar
- Igarashi, A., Pierce, B. C., and Wadler, P. 2001b. A recipe for raw types. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8) (London, UK). Available through http://www.research.att.com/~kfisher/FOOL/FOOL8.html.]]Google Scholar
- Igarashi, A. and Viroli, M. 2002. On variance-based subtyping for parametric types. In Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP) (Málaga, Spain), B. Magnusson, Ed. Lecture Notes in Computer Science, vol. 2374. Springer Verlag, Berlin, Germany 441--469.]] Google Scholar
- Interactive Software Engineering. 2001. An Eiffel tutorial. Available through http://www.eiffel.com/doc/online/eiffel50/intro/language/tutorial-00.ht%ml.]]Google Scholar
- Leroy, X. 1994. Manifest types, modules, and separate compilation. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (Portland, OR). 109--122.]] Google Scholar
- Liskov, B. 1988. Data abstraction and hierarchy. ACM SIGPLAN Notices 23, 5 (May), 17--34.]] Google Scholar
- Madsen, O. L. and Møller-Pedersen, B. 1989. Virtual classes: A powerful mechanism in object-oriented programming. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (New Orleans, LA). 397--406.]] Google Scholar
- Meyer, B. 1986. Genericity versus inheritance. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Portland, OR). 391--405.]] Google Scholar
- Meyer, B. 1992. Eiffel: The Language. Prentice Hall, Upper Saddle River, NJ.]] Google Scholar
- Mitchell, J. C. and Plotkin, G. D. 1988. Abstract types have existential types. ACM Trans. Program. Lang. Syst. 10, 3, 470--502.]] Google Scholar
- Myers, A. C., Bank, J. A., and Liskov, B. 1997. Parameterized types for Java. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (Paris, France). 132--145.]] Google Scholar
- Nordström, B., Petersson, K., and Smith, J. M. 1990. Programming in Martin-Löf's Type Theory. Oxford University Press, Oxford, UK. Out of print. An electronic version is available at http://www.cs.chalmers.se/Cs/Research/Logic/book.]]Google Scholar
- Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., and Zenger, M. 2004. An overview of the Scala programming language. Tech. Rep. IC/2004/64, École Polytechnique Fédérale de Lausanne, Switzerland.]]Google Scholar
- Odersky, M. and Wadler, P. 1997. Pizza into Java: Translating theory into practice. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (Paris, France). 146--159.]] Google Scholar
- Palacz, K. and Vitek, J. 2003. Subtype tests in real time. In Proceedings of the 17th European Conference on Object-Oriented Programming (ECOOP) (Darmstadt, Germany), L. Cardelli, Ed. Lecture Notes in Computer Science, vol. 2743. Springer Verlag, Berlin, Germany, 378--404.]]Google Scholar
- Pierce, B. C. 1994. Bounded quantification is undecidable. Inf. Comput. 112, 1 (July), 131--165. Also in Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. Carl A. Gunter and John C. Mitchell, Eds. MIT Press, Cambridge, MA.]] Google Scholar
- Pierce, B. C. and Turner, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 2 (Apr.), 207--247.]]Google Scholar
- Raynaund, O. and Thierry, E. 2001. A quasioptimal bit-vector encoding of tree hierarchies: Application to efficient type inclusion tests. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP) (Budapest, Hungary). Lecture Notes in Computer Science, vol. 2072. Springer Verlag, Berlin, Germany, 165--180.]] Google Scholar
- Steffen, M. 1998. Polarized higher-order subtyping. Ph.D. thesis, Universität Erlangen-Nürnberg.]]Google Scholar
- Sun Microsystems. 1998. Adding generic types to the Java programming language. Java Specification Request JSR-000014, http://jcp.org/jsr/detail/014.jsp.]]Google Scholar
- Syme, D. and Kennedy, A. 2001. Design and implementation of generics for the .NET common language runtime. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (Snowbird, UT). Related information is available through http://research.microsoft.com/projects/clrgen/.]] Google Scholar
- Thorup, K. K. 1997. Genericity in Java with virtual types. In Proceedings of the 11th European Conference on Object-Oriented Programming (ECOOP) (Jyväskylä, Finland). Lecture Notes in Computer Science, vol. 1241. Springer Verlag, Berlin, Germany, 444--471.]]Google Scholar
- Thorup, K. K. and Torgersen, M. 1999. Unifying genericity: Combining the benefits of virtual types and parameterized classes. In Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP) (Lisbon, Portugal). Lecture Notes in Computer Science, vol. 1628. Springer Verlag, 186--204.]] Google Scholar
- Torgersen, M. 1998. Virtual types are statically safe. In Informal Proceedings of the 5th International Workshop on Foundations of Object-Oriented Languages (FOOL5) (San Diego, CA). Available through http://www.research.att.com/~kfisher/FOOL/FOOL5.html.]]Google Scholar
- Torgersen, M., Hansen, C. P., Ernst, E., von der Ahé, P., Bracha, G., and Gafter, N. 2004. Adding wildcards to the Java programming language. In Proceedings of the ACM Symposium on Applied Computing (SAC) (Nicosia, Cyprus), 1289--1296.]] Google Scholar
- Viroli, M. 2003. A type-passing approach for the implementation of parametric methods in Java. Comput. J. 46, 3, 263--294.]]Google Scholar
- Viroli, M. and Natali, A. 2000. Parametric polymorphism in Java: An approach to translation based on reflective features. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Minneapolis, MN). 146--165.]] Google Scholar
- Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1 (Nov.), 38--94.]] Google Scholar
Index Terms
- Variant parametric types: A flexible subtyping scheme for generics
Recommendations
Featherweight Java: a minimal core calculus for Java and GJ
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step ...
Range parameterized types: use-site variance without the existential questions
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like ProgramsUse-site variance approaches such as Java wildcards allows to flexibly derive many co- and contravariant types from one generic class definition. Safety is achieved by restricting the access to members of the parameterized types, but the definition of ...
Union types for object-oriented programming
SAC '06: Proceedings of the 2006 ACM symposium on Applied computingWe propose union types for statically typed class-based object-oriented languages as a means to enhance the flexibility of subtyping. As its name suggests, a union type can be considered a set union of instances of several types and behaves as their ...
Comments