Skip to main content
SpringerLink
Log in

Foundations for Virtual Types

  • Conference paper
  • First Online:
ECOOP’ 99 — Object-Oriented Programming (ECOOP 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1628))

Included in the following conference series:

Abstract

Virtual types have been proposed as a notation for generic programming in object-oriented languages—an alternative to the more familiar mechanism of parametric classes. The tradeoffs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. However, it has proved diffcult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves are described rather informally, usually in the complicating context of full-scale language designs.

Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records. We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, dependent functions, and dependent records with both “bounded” and “manifest” type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types). Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also investigate how the partial “duality” of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Martín Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.

    Google Scholar 

  2. Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), October 1997.

    Google Scholar 

  3. Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Craig Chambers, editor, Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices volume 33 number 10, pages 183–200, Vancouver, BC, October 1998.

    Google Scholar 

  4. Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 1998. To appear in a special issue with papers from Theoretical Aspects of Computer Software (TACS), September, 1997. An earlier version appeared as an invited lecture in the Third International Workshop on Foundations of Object Oriented Languages (FOOL 3), July 1996.

    Google Scholar 

  5. Kim B. Bruce, Martin Odersky, and Philip Wadler. A statically safe alternative to virtual types. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), 1998.

    Google Scholar 

  6. Kim B. Bruce, Angela Schuett, and Robert van Gent. PolyTOIL: A type-safe polymorphic object-oriented language. In W. Olthoff, editor, Proceedings of ECOOP’ 95, LNCS 952, pages 27–51, Aarhus, Denmark, August 1995. Springer-Verlag.

    Google Scholar 

  7. Kim B. Bruce and Joseph C. Vanderwaart. Semantics-driven language design: Statically type-safe virtual types in object-oriented languages. In Fifteenth Confertence on the Mathematical Foundations of Programming Semantics, April 1999.

    Google Scholar 

  8. Luca Cardelli. Notes about F ω< . Unpublished manuscript, October 1990.

    Google Scholar 

  9. Luca Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC Systems Research Center Research Report #45, February 1989.

    Google Scholar 

  10. Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, October 1991. Preliminary version in ACM Conference on Lisp and Functional Programming, June 1990. Also available as DEC SRC Research Report 55, Feb. 1990.

    MATH  MathSciNet  Google Scholar 

  11. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, December 1985.

    Article  Google Scholar 

  12. Robert Cartwright and Guy L. Steele Jr. Compatible genericity with run-time types for the Java programming language. In Craig Chambers, editor, Object Ori-ented Programing: Systems, Languages, and Applications (OOPSLA), SIGPLAN Notices volume 33 number 10, pages 201–215, Vancouver, BC, Octover 1998. ACM.

    Google Scholar 

  13. Gang Chen and Giuseppe Longo. Subtyping parametric and dependent types. In Kamareddine et al., editor, Type Theory and Term Rewriting, September 1996. Invited lecture.

    Google Scholar 

  14. Adriana B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Computer Science Logic, September 1994. Kazimierz, Poland. Springer Lecture Notes in Computer Science 933, June 1995. Also available as University of Edinburgh, LFCS technical report ECS-LFCS-94-281, titled “Subtyping in F ∩< is decidable”.

    Google Scholar 

  15. Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, February/March 1988.

    Article  MathSciNet  MATH  Google Scholar 

  16. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, Massachusetts, 1994.

    Google Scholar 

  17. Jean-Yves Girard. Interprétation fonctionelle et élimination des couedpures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972. A summary appeared in the Proceedings of the Second Scandinavian Logic Symposium (J.E. Fenstad, editor), North-Holland, 1971 (pp. 63–92).

    Google Scholar 

  18. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the Twenty-First ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 123–137, Portland, OR, January 1994.

    Google Scholar 

  19. Martin Hofmann and Benjamin Pierce. A unifying type-theoretic framework for objects. Journal of Functional Programming, 5(4):593–635, October 1995. Previous versions appeared in the Symposium on Theoretical Aspects of Computer Science, 1994, (pages 251–262) and, under the title “An Abstract View of Objects and Subtyping (Preliminary Report),” as University of Edinburgh, LFCS technical report ECS-LFCS-92-226, 1992.

    Article  MathSciNet  Google Scholar 

  20. Xavier Leroy. Manifest types, modules and separate compilation. In Conference record of POPL’ 94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 109–122, Portland, OR, January 1994.

    Google Scholar 

  21. Mark Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 1997.

    Google Scholar 

  22. Ole Lehrmann Madsen, Boris Magnusson, and Birger Møller-Pedersen. Strong typing of object-oriented languages revisited. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) and European Conference on Object-Oriented Programming (ECOOP), pages 140–150, Ottawa, ON Canada, October 1990. ACM Press, New York, NY, USA. Published as SIGPLAN Notices, volume 25,number 10.

    Chapter  Google Scholar 

  23. Ole Lehrmann Madsen and Birger Møller-Pedersen. Virtual classes: A powerful mechanism in object-oriented programming. In Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), 1989.

    Google Scholar 

  24. Ole Lehrmann Madsen, Birger Møller-Pedersen, and Kristen Nygaard. Object-Oriented Programming in the Beta Programming Language. Addison-Wesley, 1993.

    Google Scholar 

  25. Andrew C. Myers, Joseph A. Bank, and Barbara Liskov. Parametrized types for Java. In ACM Symposium on Principles of Programming Languages (POPL), January 1997.

    Google Scholar 

  26. Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In ACM Symposium on Principles of Programming Languages (POPL), 1997.

    Google Scholar 

  27. Benjamin Pierce and Martin Steffen. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), 1994. Full version in Theoretical Computer Science, vol. 176,no. 1–2, pp. 235–282, 1997 (corrigendum in TCS vol. 184 (1997), p. 247).

    MATH  MathSciNet  Google Scholar 

  28. Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131–165, July 1994. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). A preliminary version appeared in POPL’ 92.

    Google Scholar 

  29. Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92-225, under the title “Object-Oriented Programming Without Recursive Types”.

    MATH  Google Scholar 

  30. Dedier Rémy and Jérôme Vouillon. On the (un)reality of virtual types, November 1998. manuscript.

    Google Scholar 

  31. David Shang. Are cows animals? Object Currents 1, 1996. http://www.sigs.com/objectcurrents/.

  32. Bjarne Stroustrup. The C++ Programming Language. Addison Wesley Longman, Reading, MA, tthird edition, 1997.

    Google Scholar 

  33. Kresten Krab Thorup. Genericity in Java with virtual types. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), volume 1241 of Lecture Notes in Computer Science, pages 444–471. Springer-Verlag, 1997.

    Google Scholar 

  34. Kresten Krab Thorup and Mads Torgersen. Unifying genericity: Combining the benefits of virtual types and parametrized classes. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), Springer-Verlag, June 1999.

    Google Scholar 

  35. Mads Torgersen. Vitrual types are statically safe. In 5th Workshop on Foundations of Object-Oriented Languages (FOOL), January 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer & Information Science, University of Pennsylvania, 200 South 33rd St., Philadelphia, PA, 19104, USA

    Atsushi Igarashi & Benjamin C. Pierce

Authors
  1. Atsushi Igarashi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin C. Pierce
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Swiss Federal Institute of Technology, CH-1015, Lausanne, Switzerland

    Rachid Guerraoui

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Igarashi, A., Pierce, B.C. (1999). Foundations for Virtual Types. In: Guerraoui, R. (eds) ECOOP’ 99 — Object-Oriented Programming. ECOOP 1999. Lecture Notes in Computer Science, vol 1628. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48743-3_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-48743-3_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66156-6

  • Online ISBN: 978-3-540-48743-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation