Abstract
We design and study vObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of JAVA’s inner classes as well as virtual types and family polymorphism found in BETA or GBETA. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The paper presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)
Ancona, D., Zucca, E.: A primitive calculus for module systems. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702. Springer, Heidelberg (1999)
Ancona, D., Zucca, E.: A calculus of module systems. Journal of Functional Programming (2002)
Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4), 931–940 (1983)
Bono, V., Patel, A., Shmatikov, V.: A core calculus of classes and mixins. In: Proceedings of the 13th European Conference on Object-Oriented Programming, Lisbon, Portugal, pp. 43–66 (1999)
Boudol, G.: The recursive record semantics of objects revisited. Technical Report 4199, INRIA (June 2001); To appear in Journal of Functional Programming
Bracha, G.: The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, University of Utah (1992)
Bracha, G., Griswold, D.: Extending Smalltalk with mixins. In: OOPSLA 1996 Workshop on Extending the Smalltalk Language (April 1996)
Bracha, G., Lindstrom, G.: Modularity meets inheritance. In: Proceedings of the IEEE Computer Society International Conference on Computer Languages, Washington, DC, pp. 282–290. IEEE Computer Society, Los Alamitos (1992)
Bruce, K.B.: Foundations of Object-Oriented Programming Languages: Types and Semantics. MIT Press, Cambridge (2002) ISBN 0-201-17888-5
Bruce, K.B., Fiech, A., Petersen, L.: Subtyping is not a good “Match” for object-oriented languages. In: Proceedings of the European Conference on Object-Oriented Programming, pp. 104–127 (1997)
Bruce, K.B., Odersky, M., Wadler, P.: A statical safe alternative to virtual types. In: Proceedings of the 5th International Workshop on Foundations of Object-Oriented Languages, San Diego, USA (1998)
Cardelli, L., Donahue, J., Glassman, L., Jordan, M., Kalsow, B., Nelson, G.: Modula-3 language definition. ACM SIGPLAN Notices 27(8), 15–42 (1992)
Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. Information and Computation 109(1-2), 4–56 (1994)
Cardelli, L., Mitchell, J.: Operations on records. Mathematical Structures in Computer Science 1, 3–38 (1991)
Crary, K., Harper, R., Puri, S.: What is a recursive module? In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 50–63 (1999)
Dahl, O.-J., Myhrhaug, B., Nygaard, K.: Simula: Common base language. Technical report, Norwegian Computing Center (October 1970)
Duggan, D., Sourelis, C.: Mixin modules. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pennsylvania, June 1996, pp. 262–273 (1996)
Ernst, E.: gBeta: A language with virtual attributes, block structure and propagating, dynamic inheritance. PhD thesis, Department of Computer Science, University of Aarhus, Denmark (1999)
Ernst, E.: Family polymorphism. In: Proceedings of the European Conference on Object-Oriented Programming, Budapest, Hungary, pp. 303–326 (2001)
Flatt, M., Krishnamurthi, S., Felleisen, M.: Classes and mixins. In: Proceedings of the 25th ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 171–183 (1998)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification. Java Series, 2nd edn., Sun Microsystems (2000) ISBN 0-201-31008-2
Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (January 1994)
Igarashi, A.: On inner classes. In: Proceedings of the European Conference on Object-Oriented Programming, Cannes, France (June 2000)
Igarashi, A., Pierce, B.C.: Foundations for virtual types. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, p. 161. Springer, Heidelberg (1999)
Igarashi, A., Pierce, B.C.: Foundations for virtual types. Information and Computation 175(1), 34–49 (2002)
Igarishi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: Proc. OOPSLA (November 1999)
Leroy, X.: A syntactic theory of type generativity and sharing. In: ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon (1994)
MacQueen, D.: Modules for Standard ML. In: Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, New York, August 1984, pp. 198–207 (1984)
Lehrmann Madsen, O., Møller-Pedersen, B., Nygaard, K.: Object-Oriented Programming in the BETA Programming Language. Addison-Wesley, Reading (1993) ISBN 0-201-62430-3
Madsen, O.L., Møller-Pedersen, B.: Virtual Classes: A powerful mechanism for object-oriented programming. In: Proceedings OOPSLA 1989, October 1989, pp. 397–406 (1989)
Nipkow, T., von Oheimb, D.: Java-light is type-safe — definitely. In: Cardelli, L. (ed.) Conference Record of the 25th Symposium on Principles of Programming Languages (POPL 1998), San Diego, California, pp. 161–170. ACM Press, New York (1998)
Odersky, M.: Report on the programming language Scala, École Polytechnique Fédérale de Lausanne, Switzerland (2002), http://lamp.epfl.ch/odersky/scala @
Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. Technical report IC/2002/70, EPFL, Switzerland (September 2002), http://lamp.epfl.ch/papers/technto.pdf @; Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. In: Proc. FOOL 10 (January 2003), http://www.cis.upenn.edu/~bcpierce/FOOL/FOOL10.html
Ostermann, K.: Dynamically composable collaborations with delegation layers. In: Proceedings of the 16th European Conference on Object-Oriented Programming, Málaga, Spain (2002)
Russo, C.: First-class structures for Standard ML. In: Proceedings of the 9th European Symposium on Programming, Berlin, Germany, pp. 336–350 (2000)
Smaragdakis, Y., Batory, D.: Implementing layered designs with mixin layers. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, p. 550. Springer, Heidelberg (1998)
Thorup, K.K.: Genericity in Java with virtual types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 444–471. Springer, Heidelberg (1997)
Thorup, K.K., Torgersen, M.: Unifying genericity: Combining the benefits of virtual types and parameterized classes. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, p. 186. Springer, Heidelberg (1999)
Torgersen, M.: Virtual types are statically safe. In: 5th Workshop on Foundations of Object-Oriented Languages, San Diego, CA, USA (January 1998)
Torgersen, M.: Inheritance is specialization. In: The Inheritance Workshop with ECOOP 2002 (June 2002), http://www.cs.auc.dk/eernst/inhws/ @; Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115 (1994)
Zenger, M.: Type-safe prototype-based component evolution. In: Proceedings of the European Conference on Object-Oriented Programming, Mälaga, Spain (June 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Odersky, M., Cremet, V., Röckl, C., Zenger, M. (2003). A Nominal Theory of Objects with Dependent Types. In: Cardelli, L. (eds) ECOOP 2003 – Object-Oriented Programming. ECOOP 2003. Lecture Notes in Computer Science, vol 2743. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45070-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-45070-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40531-3
Online ISBN: 978-3-540-45070-2
eBook Packages: Springer Book Archive