Variant parametric types

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Variant parametric types: A flexible subtyping scheme for generics

Full text

Pdf (557 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 28 , Issue 5 (September 2006) table of contents

Pages: 795 - 847

Year of Publication: 2006

ISSN:0164-0925

Authors

Atsushi Igarashi	Kyoto University, Kyoto, Japan
Mirko Viroli	Alma Mater Studiorum-Università di Bologna, Cesena (FC), Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 75, Citation Count: 8

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1152649.1152650 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Luca Cardelli , Ramesh Viswanathan, An interpretation of objects and object types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.396-409, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237809]
	2	Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
	3	Pierre America , Frank van der Linden, A parallel object-oriented language with inheritance and subtyping, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.161-168, September 1990, Ottawa, Canada
	4	Gilles Barthe , Maria João Frade, Constructor Subtyping, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.109-127, March 22-28, 1999
	5	Gilles Barthe , Femke van Raamsdonk, Constructor Subtyping in the Calculus of Inductive Constructions, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, p.17-34, March 25-April 02, 2000
	6	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.
	7	Gilad Bracha , David Griswold, Strongtalk: typechecking Smalltalk in a production environment, Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, p.215-230, September 26-October 01, 1993, Washington, D.C., United States
	8	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
	9	Kim B. Bruce, Safe type checking in a statically-typed object-oriented programming language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.285-298, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158650]
	10	Kim B. Bruce , Luca Cardelli , Benjamin C. Pierce, Comparing object encodings, Information and Computation, v.155 n.1-2, p.108-133, Nov./Dec. 1999 [doi>10.1006/inco.1999.2829 ]
	11	Kim B. Bruce , Martin Odersky , Philip Wadler, A Statically Safe Alternative to Virtual Types, Proceedings of the 12th European Conference on Object-Oriented Programming, p.523-549, July 20-24, 1998
	12	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.
	13	Kim B. Bruce , Angela Schuett , Robert van Gent, PolyTOIL: A Type-Safe Polymorphic Object-Oriented Language, Proceedings of the 9th European Conference on Object-Oriented Programming, p.27-51, August 07-11, 1995
	14	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.
	15	Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
	16	Cardelli, L. 1990. Notes about F^ω_<:. Unpublished manuscript.
	17	Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An extension of system F with subtyping, Information and Computation, v.109 n.1-2, p.4-56, Feb. 15/March 1994 [doi>10.1006/inco.1994.1013 ]
	18	Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
	19	Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.201-215, October 18-22, 1998, Vancouver, British Columbia, Canada
	20	Compagnoni, A. B. and Pierce, B. C. 1996. Higher-Order intersection types and multiple inheritance. Math. Struct. Comput. Sci. 6, 469--501.
	21	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.
	22	Mark Day , Robert Gruber , Barbara Liskov , Andrew C. Myers, Subtypes vs. where clauses: constraining parametric polymorphism, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.156-168, October 15-19, 1995, Austin, Texas, United States
	23	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.
	24	Giorgio Ghelli , Benjamin Pierce, Bounded existentials and minimal typing, Theoretical Computer Science, v.193 n.1-2, p.75-96, Feb. 28, 1998 [doi>10.1016/S0304-3975(96)00300-3 ]
	25	Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
	26	Atsushi Igarashi , Benjamin C. Pierce, Foundations for Virtual Types, Proceedings of the 13th European Conference on Object-Oriented Programming, p.161-185, June 14-18, 1999
	27	Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
	28	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.
	29	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
	30	Interactive Software Engineering. 2001. An Eiffel tutorial. Available through http://www.eiffel.com/doc/online/eiffel50/intro/language/tutorial-00.ht%ml.
	31	Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
	32	Barbara Liskov, Keynote address - data abstraction and hierarchy, ACM SIGPLAN Notices, v.23 n.5, p.17-34, May 1988
	33	O. L. Madsen , B. Moller-Pedersen, Virtual classes: a powerful mechanism in object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.397-406, October 02-06, 1989, New Orleans, Louisiana, United States
	34	Bertrand Meyer, Genericity versus inheritance, Conference proceedings on Object-oriented programming systems, languages and applications, p.391-405, September 29-October 02, 1986, Portland, Oregon, United States
	35	Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
	36	John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
	37	Joseph A. Bank , Andrew C. Myers , Barbara Liskov, Parameterized types for Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.132-145, January 15-17, 1997, Paris, France [doi>10.1145/263699.263714]
	38	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.
	39	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.
	40	Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
	41	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.
	42	Benjamin C. Pierce, Bounded quantification is undecidable, Information and Computation, v.112 n.1, p.131-165, July 1994 [doi>10.1006/inco.1994.1055 ]
	43	Pierce, B. C. and Turner, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 2 (Apr.), 207--247.
	44	Olivier Raynaud , Eric Thierry, A Quasi Optimal Bit-Vector Encoding of Tree Hierarchies. Application to Efficient Type Inclusion Tests, Proceedings of the 15th European Conference on Object-Oriented Programming, p.165-180, June 18-22, 2001
	45	Steffen, M. 1998. Polarized higher-order subtyping. Ph.D. thesis, Universität Erlangen-Nürnberg.
	46	Sun Microsystems. 1998. Adding generic types to the Java programming language. Java Specification Request JSR-000014, http://jcp.org/jsr/detail/014.jsp.
	47	Andrew Kennedy , Don Syme, Design and implementation of generics for the .NET Common language runtime, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.1-12, June 2001, Snowbird, Utah, United States
	48	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.
	49	Kresten Krab Thorup , Mads Torgersen, Unifying Genericity - Combining the Benefits of Virtual Types and Parameterized Classes, Proceedings of the 13th European Conference on Object-Oriented Programming, p.186-204, June 14-18, 1999
	50	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.
	51	Mads Torgersen , Christian Plesner Hansen , Erik Ernst , Peter von der Ahé , Gilad Bracha , Neal Gafter, Adding wildcards to the Java programming language, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus [doi>10.1145/967900.968162]
	52	Viroli, M. 2003. A type-passing approach for the implementation of parametric methods in Java. Comput. J. 46, 3, 263--294.
	53	Mirko Viroli , Antonio Natali, Parametric polymorphism in Java: an approach to translation based on reflective features, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.146-165, October 2000, Minneapolis, Minnesota, United States
	54	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 ]

CITED BY 8

	Maurizio Cimadamore , Mirko Viroli, Reifying wildcards in Java using the EGO approach, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
	Alessandro Ricci , Mirko Viroli , Maurizio Cimadamore, Prototyping Concurrent Systems with Agents and Artifacts: Framework and Core Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), v.194 n.4, p.111-132, April, 2008
	Maurizio Cimadamore , Mirko Viroli, Integrating Java and Prolog through generic methods and type inference, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil
	Maurizio Cimadamore , Mirko Viroli, A Prolog-oriented extension of Java programming based on generics and annotations, Proceedings of the 5th international symposium on Principles and practice of programming in Java, September 05-07, 2007, Lisboa, Portugal
	Shan Shan Huang , David Zook , Yannis Smaragdakis, cJ: enhancing java with safe type conditions, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada
	Atsushi Igarashi , Mirko Viroli, Variant path types for scalable extensibility, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Wei-Ngan Chin , Florin Craciun , Siau-Cheng Khoo , Corneliu Popeea, A flow-based approach for variant parametric types, ACM SIGPLAN Notices, v.41 n.10, October 2006
	Yoav Zibin , Alex Potanin , Mahmood Ali , Shay Artzi , Adam Kie\|un , Michael D. Ernst, Object and reference immutability using Java generics, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia